Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-05-04 13:44 570e9f48

View on Github →

feat(ring_theory/localization/away) : Add num_denom section (#18830) Added a section num_denom: the main result is the lemma exists_reduced_fraction that shows that every non-zero element b in a localization.away x of a UFM can be written in a unique way as b=x^n * a with n : ℤ and a not divisible by x.

Estimated changes

added theorem self_zpow_add
added theorem self_zpow_coe_nat
added theorem self_zpow_mul_neg
added theorem self_zpow_neg_coe_nat
added theorem self_zpow_neg_mul
added theorem self_zpow_of_neg
added theorem self_zpow_of_nonneg
added theorem self_zpow_of_nonpos
added theorem self_zpow_pow_sub
added theorem self_zpow_sub_cast_nat
added theorem self_zpow_zero