Commit 2026-06-02 14:56 6322bf65

View on Github →

chore: switch EqLocus from LinearMapClass to LinearMap (#39487)

Estimated changes

Modified Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

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

modified def LinearMap.eqLocus

modified theorem LinearMap.eqLocus_eq_top

modified theorem LinearMap.eqLocus_same

modified theorem LinearMap.eqLocus_toAddSubmonoid

modified theorem LinearMap.eqOn_sup

modified theorem LinearMap.le_eqLocus

modified theorem LinearMap.mem_eqLocus

Modified Mathlib/Analysis/InnerProductSpace/MeanErgodic.lean

Modified Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean