Prove BogomolovPopInjectivity (openai/math family 009: Bogomolov–Pop and Milnor $K$-theoretic…
Prove BogomolovPopInjectivity (openai/math family 009: Bogomolov–Pop and Milnor $K$-theoretic…: a task in openai/math as Harbor environments (Harbor dataset). Context: this statement belongs to family 009 of the release, Bogomolov–Pop and Milnor $K$-theoretic reconstruction (Number theory). The…
The task
Context: this statement belongs to family 009 of the release, *Bogomolov–Pop and Milnor $K$-theoretic reconstruction* (Number theory). The family as a whole: Reconstructs function fields of transcendence degree at least two over algebraically closed constants from $K^{\mathrm M}_1/\ell$, $K^{\mathrm M}_2/\ell$, and…
Part of raising-heart/openai-math.