Commit 2025-04-08 12:11 12069db6

View on Github →

chore(LinearAlgebra): process misc porting notes (#23795)

Estimated changes

Modified Mathlib/LinearAlgebra/Basis/Defs.lean

Modified Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean

Modified Mathlib/LinearAlgebra/Finsupp/Span.lean

Modified Mathlib/LinearAlgebra/LinearIndependent/Basic.lean

Modified Mathlib/LinearAlgebra/Span/Defs.lean

deleted theorem Submodule.IsPrincipal.principal

Modified Mathlib/RingTheory/FractionalIdeal/Operations.lean

Modified Mathlib/RingTheory/Ideal/IsPrincipalPowQuotient.lean

Modified Mathlib/RingTheory/SimpleModule/Basic.lean