Commit 2023-02-15 01:06 3a8b0135

View on Github →

feat: port Topology.Algebra.GroupWithZero (#2288)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Algebra/GroupWithZero.lean

added theorem Continuous.comp_div_cases

added theorem Continuous.div

added theorem Continuous.div_const

added theorem Continuous.inv₀

added theorem Continuous.zpow₀

added theorem ContinuousAt.comp_div_cases

added theorem ContinuousOn.div

added theorem ContinuousOn.div_const

added theorem ContinuousOn.inv₀

added theorem ContinuousOn.zpow₀

added theorem Filter.Tendsto.div

added theorem Filter.Tendsto.div_const

added theorem Filter.Tendsto.inv₀

added theorem Filter.Tendsto.zpow₀

added theorem Filter.tendsto_mul_iff_of_ne_zero

added theorem Homeomorph.coe_mulLeft₀

added theorem Homeomorph.coe_mulRight₀

added theorem Homeomorph.mulLeft₀_symm_apply

added theorem Homeomorph.mulRight₀_symm_apply

added theorem continuousAt_zpow₀

added theorem continuousOn_div

added theorem continuousOn_inv₀

added theorem continuousOn_zpow₀

added theorem tendsto_inv₀