Commit 2023-05-26 05:11 e18a7afa

View on Github →

feat: port RingTheory.IntegralDomain (#4362)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/IntegralDomain.lean

added theorem Finite.isField_of_domain

added theorem Finset.exists_eq_pow_of_mul_eq_pow_of_coprime

added def Fintype.divisionRingOfIsDomain

added def Fintype.fieldOfDomain

added def Fintype.groupWithZeroOfCancel

added theorem Polynomial.div_eq_quo_add_rem_div

added theorem card_fiber_eq_of_mem_range

added theorem card_nthRoots_subgroup_units

added theorem exists_eq_pow_of_mul_eq_pow_of_coprime

added theorem isCyclic_of_subgroup_isDomain

added theorem mul_left_bijective_of_finite₀

added theorem mul_right_bijective_of_finite₀

added theorem sum_hom_units

added theorem sum_hom_units_eq_zero