Theorem Module.Finite.exists_nat_not_surjective

Modification history

2025-05-11 00:56
Mathlib/LinearAlgebra/InvariantBasisNumber.lean
chore(LinearAlgebra/Dual): generalize to semirings (#23933)
Added Module.Finite.exists_nat_not_surjectiveView on Github →