Theorem OreLocalization.cardinalMk_le_lift_cardinalMk_of_commute

Modification history

2024-11-11 08:54
Mathlib/GroupTheory/OreLocalization/Cardinality.lean
feat: add results on cardinality of localization (#18004) …
Added OreLocalization.cardinalMk_le_lift_cardinalMk_of_commuteView on Github →