Commit 2026-07-23 01:41 b5d557f7

View on Github →

refactor(LinearAlgebra): semilinearize Submodule.Quotient.equiv (#42001) This PR generalizes Submodule.Quotient.equiv to a semi-linear equivalence.

Estimated changes

Modified Mathlib/LinearAlgebra/Quotient/Basic.lean

modified def Submodule.Quotient.equiv

added theorem Submodule.Quotient.equiv_apply

modified theorem Submodule.Quotient.equiv_symm

modified theorem Submodule.Quotient.equiv_trans