Commit 2025-12-08 23:04 89e3baf4

View on Github →

chore(LinearAlgebra/Dimension): generalize and golf (#32339) LinearAlgebra/Dimension/Finite.lean: generalize Ring/AddCommGroup to Semiring/AddCommMonoid whenever possible LinearAlgebra/Dimension/DivisionRing.lean: generalize DivisionRing to OrzechProperty, move to new file OrzechProperty.lean

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Module/ZLattice/Basic.lean

Modified Mathlib/FieldTheory/PerfectClosure.lean

Modified Mathlib/FieldTheory/PurelyInseparable/PerfectClosure.lean

Modified Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean

Modified Mathlib/LinearAlgebra/Dimension/DivisionRing.lean

deleted theorem coe_basisOfTopLeSpanOfCardEqFinrank

deleted theorem linearIndependent_iff_card_eq_finrank_span

deleted theorem linearIndependent_iff_card_le_finrank_span

deleted theorem linearIndependent_of_top_le_span_of_card_eq_finrank

Modified Mathlib/LinearAlgebra/Dimension/Finite.lean

modified theorem Module.finite_of_rank_eq_zero

modified theorem Module.nontrivial_of_finrank_pos

modified theorem rank_eq_zero_iff

added theorem rank_le_one

Created Mathlib/LinearAlgebra/Dimension/OrzechProperty.lean

added theorem coe_basisOfTopLeSpanOfCardEqFinrank

added theorem linearIndependent_iff_card_eq_finrank_span

added theorem linearIndependent_iff_card_le_finrank_span

added theorem linearIndependent_of_top_le_span_of_card_eq_finrank

added theorem linearIndependent_of_top_le_span_of_card_le_finrank

Modified Mathlib/LinearAlgebra/Matrix/Rank.lean

Modified Mathlib/RingTheory/LocalRing/Quotient.lean