Commit 2023-09-07 20:17 a8cb5022

View on Github →

chore: tidy various files (#7017)

Estimated changes

Modified Mathlib/Algebra/Module/Zlattice.lean

deleted def Zspan.QuotientEquiv

added def Zspan.fractRestrict

added theorem Zspan.fractRestrict_apply

added theorem Zspan.fractRestrict_surjective

deleted def Zspan.fract_restrict

deleted theorem Zspan.fract_restrict_apply

deleted theorem Zspan.fract_restrict_surjective

added def Zspan.quotientEquiv

Modified Mathlib/Algebra/Order/CompleteField.lean

Modified Mathlib/Analysis/NormedSpace/Connected.lean

Modified Mathlib/Analysis/NormedSpace/OperatorNorm.lean

Modified Mathlib/CategoryTheory/Monoidal/Internal/Limits.lean

Modified Mathlib/CategoryTheory/Monoidal/Internal/Module.lean

Modified Mathlib/Data/Matrix/Invertible.lean

Modified Mathlib/Data/Nat/Squarefree.lean

Modified Mathlib/Data/PFun.lean

Modified Mathlib/LinearAlgebra/Dimension.lean

added theorem exists_linearIndependent_cons_of_lt_rank

added theorem exists_linearIndependent_pair_of_one_lt_rank

added theorem exists_linearIndependent_snoc_of_lt_rank

deleted theorem exists_linear_independent_cons_of_lt_rank

deleted theorem exists_linear_independent_pair_of_one_lt_rank

deleted theorem exists_linear_independent_snoc_of_lt_rank

Modified Mathlib/LinearAlgebra/FiniteDimensional.lean

Modified Mathlib/LinearAlgebra/Finrank.lean

added theorem exists_linearIndependent_cons_of_lt_finrank

added theorem exists_linearIndependent_pair_of_one_lt_finrank

added theorem exists_linearIndependent_snoc_of_lt_finrank

deleted theorem exists_linear_independent_cons_of_lt_finrank

deleted theorem exists_linear_independent_pair_of_one_lt_finrank

deleted theorem exists_linear_independent_snoc_of_lt_finrank

Modified Mathlib/MeasureTheory/Function/LpSeminorm.lean

Modified Mathlib/MeasureTheory/Integral/Average.lean

Modified Mathlib/RingTheory/Localization/Basic.lean

modified def Localization.mkAddMonoidHom

Modified Mathlib/RingTheory/TensorProduct.lean

Modified Mathlib/Topology/Algebra/Module/Cardinality.lean

added theorem cardinal_eq_of_isOpen

deleted theorem cardinal_eq_of_is_open

added theorem continuum_le_cardinal_of_isOpen

deleted theorem continuum_le_cardinal_of_is_open

Modified Mathlib/Topology/Category/Stonean/EffectiveEpi.lean