Commit 2024-07-02 22:51 4180b90a

View on Github →

refactor(LinearAlgebra,RingTheory): Replace Fintype.card with Nat.card (#13637) This PR replaces a few occurrences of Fintype.card with Nat.card in the LinearAlgebra and RingTheory folders.

Estimated changes

Modified Mathlib/LinearAlgebra/Isomorphisms.lean

modified theorem Submodule.card_quotient_mul_card_quotient

Modified Mathlib/LinearAlgebra/Quotient.lean

modified theorem Submodule.card_eq_card_quotient_mul_card

Modified Mathlib/NumberTheory/Cyclotomic/Rat.lean

Modified Mathlib/RingTheory/Ideal/Norm.lean

modified theorem Submodule.cardQuot_apply

modified theorem cardQuot_mul

modified theorem cardQuot_mul_of_coprime

modified theorem cardQuot_pow_of_prime