Commit 2023-05-21 12:23 bbc61ef8

View on Github →

feat: port RingTheory.GradedAlgebra.HomogeneousLocalization (#4155)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean

added theorem HomogeneousLocalization.NumDenSameDeg.deg_add

added theorem HomogeneousLocalization.NumDenSameDeg.deg_mul

added theorem HomogeneousLocalization.NumDenSameDeg.deg_neg

added theorem HomogeneousLocalization.NumDenSameDeg.deg_one

added theorem HomogeneousLocalization.NumDenSameDeg.deg_pow

added theorem HomogeneousLocalization.NumDenSameDeg.deg_smul

added theorem HomogeneousLocalization.NumDenSameDeg.deg_zero

added theorem HomogeneousLocalization.NumDenSameDeg.den_add

added theorem HomogeneousLocalization.NumDenSameDeg.den_mul

added theorem HomogeneousLocalization.NumDenSameDeg.den_neg

added theorem HomogeneousLocalization.NumDenSameDeg.den_one

added theorem HomogeneousLocalization.NumDenSameDeg.den_pow

added theorem HomogeneousLocalization.NumDenSameDeg.den_smul

added theorem HomogeneousLocalization.NumDenSameDeg.den_zero

added def HomogeneousLocalization.NumDenSameDeg.embedding

added theorem HomogeneousLocalization.NumDenSameDeg.ext

added theorem HomogeneousLocalization.NumDenSameDeg.num_add

added theorem HomogeneousLocalization.NumDenSameDeg.num_mul

added theorem HomogeneousLocalization.NumDenSameDeg.num_neg

added theorem HomogeneousLocalization.NumDenSameDeg.num_one

added theorem HomogeneousLocalization.NumDenSameDeg.num_pow

added theorem HomogeneousLocalization.NumDenSameDeg.num_smul

added theorem HomogeneousLocalization.NumDenSameDeg.num_zero

added structure HomogeneousLocalization.NumDenSameDeg

added theorem HomogeneousLocalization.add_val

added def HomogeneousLocalization.deg

added def HomogeneousLocalization.den

added theorem HomogeneousLocalization.den_mem

added theorem HomogeneousLocalization.den_mem_deg

added theorem HomogeneousLocalization.eq_num_div_den

added theorem HomogeneousLocalization.ext_iff_val

added theorem HomogeneousLocalization.intCast_val

added theorem HomogeneousLocalization.isUnit_iff_isUnit_val

added theorem HomogeneousLocalization.mul_val

added theorem HomogeneousLocalization.natCast_val

added theorem HomogeneousLocalization.neg_val

added def HomogeneousLocalization.num

added theorem HomogeneousLocalization.num_mem_deg

added theorem HomogeneousLocalization.one_eq

added theorem HomogeneousLocalization.one_val

added theorem HomogeneousLocalization.pow_val

added theorem HomogeneousLocalization.smul_val

added theorem HomogeneousLocalization.sub_val

added def HomogeneousLocalization.val

added theorem HomogeneousLocalization.val_injective

added theorem HomogeneousLocalization.val_mk''

added theorem HomogeneousLocalization.zero_eq

added theorem HomogeneousLocalization.zero_val

added def HomogeneousLocalization