Mathlib Changelog
v4
Changelog
About
Github
Commit
2026-10-28 16:14
97bcf245
View on Github →
feat: use
IsApply
for
Module.End
(
#45347
)
Estimated changes
Modified
Mathlib/Algebra/Central/End.lean
Modified
Mathlib/Algebra/Group/ForwardDiff.lean
Modified
Mathlib/Algebra/Lie/CartanExists.lean
Modified
Mathlib/Algebra/Lie/Derivation/Basic.lean
Modified
Mathlib/Algebra/Lie/EngelSubalgebra.lean
Modified
Mathlib/Algebra/Lie/LieTheorem.lean
Modified
Mathlib/Algebra/Lie/Nilpotent.lean
Modified
Mathlib/Algebra/Lie/OfAssociative.lean
Modified
Mathlib/Algebra/Lie/Sl2.lean
Modified
Mathlib/Algebra/Lie/Weights/Basic.lean
Modified
Mathlib/Algebra/Lie/Weights/Cartan.lean
Modified
Mathlib/Algebra/Module/Equiv/Basic.lean
Modified
Mathlib/Algebra/Module/FinitePresentation.lean
Modified
Mathlib/Algebra/Module/LinearMap/End.lean
deleted
theorem
Module.End.intCast_apply
deleted
theorem
Module.End.mul_apply
deleted
theorem
Module.End.natCast_apply
deleted
theorem
Module.End.one_apply
deleted
theorem
Module.End.pow_apply
Modified
Mathlib/Algebra/Module/Submodule/Ker.lean
Modified
Mathlib/Algebra/Module/Submodule/LinearMap.lean
Modified
Mathlib/Algebra/Polynomial/Derivative.lean
Modified
Mathlib/Algebra/Polynomial/Module/Basic.lean
Modified
Mathlib/Analysis/Calculus/LagrangeMultipliers.lean
Modified
Mathlib/Analysis/InnerProductSpace/Adjoint.lean
Modified
Mathlib/Analysis/InnerProductSpace/Positive.lean
Modified
Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean
Modified
Mathlib/Analysis/InnerProductSpace/Symmetric.lean
Modified
Mathlib/FieldTheory/Finite/Basic.lean
Modified
Mathlib/FieldTheory/Galois/NormalBasis.lean
Modified
Mathlib/FieldTheory/JacobsonNoether.lean
Modified
Mathlib/LinearAlgebra/Center.lean
Modified
Mathlib/LinearAlgebra/Dual/Lemmas.lean
Modified
Mathlib/LinearAlgebra/Eigenspace/Basic.lean
Modified
Mathlib/LinearAlgebra/Eigenspace/Minpoly.lean
Modified
Mathlib/LinearAlgebra/Eigenspace/Pi.lean
Modified
Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean
Modified
Mathlib/LinearAlgebra/Eigenspace/Zero.lean
Modified
Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean
Modified
Mathlib/LinearAlgebra/FreeModule/Basic.lean
Modified
Mathlib/LinearAlgebra/GeneralLinearGroup/AlgEquiv.lean
Modified
Mathlib/LinearAlgebra/Matrix/Charpoly/LinearMap.lean
Modified
Mathlib/LinearAlgebra/Matrix/ToLin.lean
Modified
Mathlib/LinearAlgebra/PiTensorProduct/Dual.lean
Modified
Mathlib/LinearAlgebra/Projection.lean
Modified
Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
Modified
Mathlib/LinearAlgebra/Reflection.lean
Modified
Mathlib/LinearAlgebra/Semisimple.lean
Modified
Mathlib/LinearAlgebra/Span/Basic.lean
Modified
Mathlib/LinearAlgebra/Transvection/Generation.lean
Modified
Mathlib/RepresentationTheory/Basic.lean
Modified
Mathlib/RepresentationTheory/Coinduced.lean
Modified
Mathlib/RepresentationTheory/FiniteIndex.lean
Modified
Mathlib/RepresentationTheory/Homological/GroupCohomology/Functoriality.lean
Modified
Mathlib/RepresentationTheory/Homological/GroupCohomology/LowDegree.lean
Modified
Mathlib/RepresentationTheory/Homological/GroupHomology/FiniteCyclic.lean
Modified
Mathlib/RepresentationTheory/Intertwining.lean
Modified
Mathlib/RepresentationTheory/Invariants.lean
Modified
Mathlib/RepresentationTheory/Stabilizer.lean
Modified
Mathlib/RingTheory/Artinian/Module.lean
Modified
Mathlib/RingTheory/Derivation/Lie.lean
Modified
Mathlib/RingTheory/Extension/Cotangent/LocalizationAway.lean
Modified
Mathlib/RingTheory/Noetherian/Defs.lean
Modified
Mathlib/RingTheory/Polynomial/Basic.lean
Modified
Mathlib/RingTheory/Polynomial/Bernstein.lean