Commit 2024-10-23 01:35 cd8e93f7

View on Github →

chore: generalize from AddCommGroup to AddCommMonoid (#18095) This lets many theorems apply to M := R where R is a ring.

Estimated changes

Modified Mathlib/LinearAlgebra/Basis/Cardinality.lean

Modified Mathlib/LinearAlgebra/FreeModule/Finite/Basic.lean

Modified Mathlib/RingTheory/Finiteness.lean

modified theorem Module.Finite.finite_basis