Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-10-09 09:42
9902eed0
View on Github →
chore: remove more unused variables (
#17551
)
Estimated changes
Modified
Mathlib/Algebra/Field/Defs.lean
Modified
Mathlib/Algebra/Group/Action/Defs.lean
Modified
Mathlib/Algebra/Group/Action/Opposite.lean
Modified
Mathlib/Algebra/Group/Action/Sum.lean
Modified
Mathlib/Algebra/Group/Defs.lean
Modified
Mathlib/Algebra/Group/Equiv/Basic.lean
Modified
Mathlib/Algebra/Group/Even.lean
Modified
Mathlib/Algebra/Group/Hom/Basic.lean
Modified
Mathlib/Algebra/Group/Hom/End.lean
Modified
Mathlib/Algebra/Group/Prod.lean
Modified
Mathlib/Algebra/Group/Units.lean
Modified
Mathlib/Algebra/Group/Units/Equiv.lean
Modified
Mathlib/Algebra/Group/Units/Hom.lean
Modified
Mathlib/Algebra/Group/WithOne/Defs.lean
Modified
Mathlib/Algebra/GroupWithZero/Action/Defs.lean
Modified
Mathlib/Algebra/GroupWithZero/Action/Opposite.lean
Modified
Mathlib/Algebra/GroupWithZero/Action/Prod.lean
Modified
Mathlib/Algebra/GroupWithZero/Basic.lean
Modified
Mathlib/Algebra/GroupWithZero/Defs.lean
Modified
Mathlib/Algebra/GroupWithZero/InjSurj.lean
Modified
Mathlib/Algebra/GroupWithZero/Pi.lean
Modified
Mathlib/Algebra/GroupWithZero/Units/Basic.lean
Modified
Mathlib/Algebra/GroupWithZero/Units/Lemmas.lean
Modified
Mathlib/Algebra/Module/LinearMap/Basic.lean
modified
theorem
DomMulAct.coe_smul_linearMap
modified
theorem
DomMulAct.mk_smul_linearMap_apply
modified
theorem
DomMulAct.smul_linearMap_apply
Modified
Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
Modified
Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
Modified
Mathlib/Algebra/Order/Monoid/Defs.lean
Modified
Mathlib/Algebra/Order/Monoid/Unbundled/Defs.lean
Modified
Mathlib/Algebra/Order/Monoid/Unbundled/Pow.lean
Modified
Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean
Modified
Mathlib/Algebra/Ring/Commute.lean
Modified
Mathlib/Algebra/Ring/Defs.lean
Modified
Mathlib/Control/Monad/Cont.lean
Modified
Mathlib/Control/Monad/Writer.lean
Modified
Mathlib/Control/Traversable/Basic.lean
Modified
Mathlib/Control/Traversable/Lemmas.lean
Modified
Mathlib/Data/Countable/Basic.lean
Modified
Mathlib/Data/Matrix/DMatrix.lean
Modified
Mathlib/Data/Nat/Cast/Commute.lean
Modified
Mathlib/Data/Nat/Cast/Synonym.lean
Modified
Mathlib/Data/Nat/Defs.lean
Modified
Mathlib/Data/Nat/Find.lean
Modified
Mathlib/Data/Prod/Lex.lean
Modified
Mathlib/Data/Sigma/Lex.lean
Modified
Mathlib/Deprecated/Group.lean
Modified
Mathlib/Init/Algebra/Classes.lean
Modified
Mathlib/LinearAlgebra/LinearIndependent.lean
Modified
Mathlib/Logic/Basic.lean
Modified
Mathlib/Logic/Equiv/Basic.lean
Modified
Mathlib/Logic/Function/Basic.lean
Modified
Mathlib/Logic/Pairwise.lean
Modified
Mathlib/Logic/Relation.lean
Modified
Mathlib/Order/BoundedOrder.lean
Modified
Mathlib/Order/Heyting/Basic.lean
Modified
Mathlib/Order/Hom/Basic.lean
Modified
Mathlib/Order/Max.lean
Modified
Mathlib/Order/Monotone/Basic.lean
Modified
Mathlib/Order/Monotone/Monovary.lean
Modified
Mathlib/Order/Synonym.lean
Modified
Mathlib/Order/WithBot.lean
Modified
Mathlib/Topology/LocallyFinite.lean