Commit 2025-03-15 16:04 14bdbbdf

View on Github →

chore(Ideal/Quotient): change Fintype to Finite (#22947) As discussed here

Estimated changes

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

added theorem Submodule.finiteQuotientOfFreeOfRankEq

Modified Mathlib/LinearAlgebra/FreeModule/IdealQuotient.lean

added theorem Ideal.finiteQuotientOfFreeOfNeBot

Modified Mathlib/NumberTheory/Cyclotomic/Rat.lean

modified theorem IsPrimitiveRoot.card_quotient_toInteger_sub_one

Modified Mathlib/NumberTheory/Cyclotomic/Three.lean

Modified Mathlib/NumberTheory/NumberField/FinitePlaces.lean

Modified Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean