Commit 2023-03-06 06:48 0a4af621

View on Github →

feat: port Topology.Algebra.Order.Field (#2626) I made substantial changes to the proofs. To avoid backporting most of them, in leanprover-community/mathlib#18552 I add private to lemmas that are deleted in this PR. Also, I backport Homeomorph.symm_symm in leanprover-community/mathlib#18551

Estimated changes

deleted theorem Filter.Tendsto.div_div
deleted theorem Filter.Tendsto.inv_inv
modified theorem Homeomorph.coe_mulLeft₀
modified theorem Homeomorph.coe_mulRight₀
added theorem map_mul_left_nhds₀
added theorem map_mul_right_nhds₀
added theorem tendsto_inv_atTop_zero
added theorem tendsto_inv_zero_atTop
added theorem tendsto_pow_neg_atTop
added theorem Homeomorph.symm_symm