Theorem IsFractionRing.num_den_reduced

Modification history

2024-02-12 20:59

Mathlib/RingTheory/Localization/NumDen.lean

feat: introduce `IsRelPrime` and `DecompositionMonoid` and refactor (#10327) …

Modified IsFractionRing.num_den_reduced View on Github →

2023-03-23 14:22

Mathlib/RingTheory/Localization/NumDen.lean

feat: port RingTheory.Localization.NumDen (#3044)

Added IsFractionRing.num_den_reduced View on Github →