Commit 2023-05-22 12:09 c6afc89a

View on Github →

feat: port RingTheory.Localization.Cardinality (#4192)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Localization/Cardinality.lean

added theorem IsLocalization.card

added theorem IsLocalization.card_le