Commit 2026-07-01 13:18 dc54c899

View on Github →

chore(NumberTheory/NumberField/Units/Basic): use Nat.card instead of Fintype.card (#41210) This PR switches NumberTheory/NumberField/Units/Basic.lean and some downstream files from Fintype.card to Nat.card.

Estimated changes

Modified Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean

modified theorem modularCyclotomicCharacter.toFun_unique'

modified theorem modularCyclotomicCharacter.toFun_unique

Modified Mathlib/NumberTheory/NumberField/CMField.lean

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean

Modified Mathlib/NumberTheory/NumberField/Cyclotomic/Basic.lean

modified theorem NumberField.Units.dvd_torsionOrder_of_isPrimitiveRoot

Modified Mathlib/NumberTheory/NumberField/Ideal/Basic.lean

Modified Mathlib/NumberTheory/NumberField/Units/Basic.lean

modified def NumberField.Units.torsionOrder

modified theorem NumberField.Units.torsionOrder_ne_zero

modified theorem NumberField.Units.torsionOrder_pos

Modified Mathlib/RingTheory/RootsOfUnity/Basic.lean

modified theorem card_rootsOfUnity

Modified Mathlib/RingTheory/RootsOfUnity/Complex.lean

modified theorem Complex.card_rootsOfUnity

Modified Mathlib/RingTheory/RootsOfUnity/EnoughRootsOfUnity.lean

Modified Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean

Modified Mathlib/RingTheory/ZMod/Torsion.lean