`BookProof.ChapterFreeFieldBornSurj.bornMap_bornSection` {p : Fin n → ℝ} (hp : p ∈ stdSimplex ℝ (Fin n)) : bornMap (bornSection p) = p

Initializing...

`BookProof.ChapterFreeFieldBornSurj.bornMap_bornSection` {p : Fin n → ℝ} (hp : p ∈ stdSimplex ℝ (Fin n)) : bornMap (bornSection p) = p · Prove2Me