Commit 2023-03-04 17:31 be307bad

View on Github →

feat: port Topology.Algebra.Field (#2617)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Algebra/Field.lean

added theorem Filter.tendsto_cocompact_mul_left₀

added theorem Filter.tendsto_cocompact_mul_right₀

added theorem IsLocalMin.inv

added theorem IsPreconnected.eq_of_sq_eq

added theorem IsPreconnected.eq_one_or_eq_neg_one_of_sq_eq

added theorem IsPreconnected.eq_or_eq_neg_of_sq_eq

added theorem Subfield.isClosed_topologicalClosure

added theorem Subfield.le_topologicalClosure

added def Subfield.topologicalClosure

added theorem Subfield.topologicalClosure_minimal

added def affineHomeomorph

Modified Mathlib/Topology/Connected.lean

added theorem IsPreconnected.eqOn_const_of_mapsTo