Commit 2023-05-21 22:17 db7cc7d2

View on Github →

feat: port RingTheory.Localization.Away.Basic (#4139)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Init/Data/Int/Basic.lean

added theorem Int.natAbs_add_neg

added theorem Int.natAbs_add_nonneg

Created Mathlib/RingTheory/Localization/Away/Basic.lean

added theorem IsLocalization.Away.AwayMap.lift_comp

added theorem IsLocalization.Away.AwayMap.lift_eq

added theorem IsLocalization.Away.mul_invSelf

added theorem IsLocalization.away_of_isUnit_of_bijective

added theorem exists_reduced_fraction'

added theorem selfZpow_add

added theorem selfZpow_coe_nat

added theorem selfZpow_mul_neg

added theorem selfZpow_neg_coe_nat

added theorem selfZpow_neg_mul

added theorem selfZpow_of_neg

added theorem selfZpow_of_nonneg

added theorem selfZpow_of_nonpos

added theorem selfZpow_pow_sub

added theorem selfZpow_sub_cast_nat

added theorem selfZpow_zero