Commit 2023-02-12 15:02 a2ebfa0b

View on Github →

chore: tidy various files (#2236)

Estimated changes

Modified Mathlib/Algebra/Hom/Freiman.lean

added theorem FreimanHom.toFun_eq_coe

deleted theorem FreimanHom.to_fun_eq_coe

modified def FreimanHomClass.toFreimanHom

Modified Mathlib/Algebra/Module/Submodule/Lattice.lean

modified def AddSubgroup.toIntSubmodule

modified def AddSubmonoid.toNatSubmodule

modified def Submodule.botEquivPUnit

deleted theorem Submodule.sum_mem_bsupr

added theorem Submodule.sum_mem_bsupᵢ

modified def Submodule.topEquiv

Modified Mathlib/Algebra/Order/Pointwise.lean

Modified Mathlib/Data/Finmap.lean

Modified Mathlib/Data/Finset/Preimage.lean

Modified Mathlib/Data/Multiset/Basic.lean

Modified Mathlib/GroupTheory/Coset.lean

Modified Mathlib/GroupTheory/DoubleCoset.lean

Modified Mathlib/Order/Filter/IndicatorFunction.lean

deleted theorem tendsto_indicator_bUnion_finset

added theorem tendsto_indicator_bunionᵢ_finset

Modified Mathlib/Order/Filter/Partial.lean

modified def Filter.rcomap'

modified def Filter.rcomap

modified def Filter.rmap

Modified Mathlib/Order/Heyting/Hom.lean

Modified Mathlib/RingTheory/NonZeroDivisors.lean

added theorem mul_cancel_left_coe_nonZeroDivisors

deleted theorem mul_cancel_left_coe_non_zero_divisor

added theorem mul_cancel_left_mem_nonZeroDivisors

deleted theorem mul_cancel_left_mem_non_zero_divisor

added theorem mul_cancel_right_coe_nonZeroDivisors

deleted theorem mul_cancel_right_coe_non_zero_divisor

added theorem mul_cancel_right_mem_nonZeroDivisors

deleted theorem mul_cancel_right_mem_non_zero_divisor

modified def nonZeroDivisors

Modified Mathlib/RingTheory/OreLocalization/Basic.lean

Modified Mathlib/Topology/ContinuousFunction/CocompactMap.lean

added theorem CocompactMap.coe_toContinuousMap

deleted theorem CocompactMap.coe_to_continuous_fun

Modified Mathlib/Topology/UniformSpace/Cauchy.lean

modified theorem CauchySeq.totallyBounded_range