Commit 2023-05-17 06:12 c948d8a7

View on Github →

feat: port RingTheory.FreeCommRing (#3994)

depends on: #3414 original: #3087

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/FreeCommRing.lean

added def FreeCommRing.IsSupported

added theorem FreeCommRing.exists_finite_support

added theorem FreeCommRing.exists_finset_support

added theorem FreeCommRing.hom_ext

added theorem FreeCommRing.isSupported_add

added theorem FreeCommRing.isSupported_int

added theorem FreeCommRing.isSupported_mul

added theorem FreeCommRing.isSupported_neg

added theorem FreeCommRing.isSupported_of

added theorem FreeCommRing.isSupported_one

added theorem FreeCommRing.isSupported_sub

added theorem FreeCommRing.isSupported_upwards

added theorem FreeCommRing.isSupported_zero

added def FreeCommRing.lift

added theorem FreeCommRing.lift_comp_of

added theorem FreeCommRing.lift_of

added def FreeCommRing.map

added theorem FreeCommRing.map_of

added theorem FreeCommRing.map_subtype_val_restriction

added def FreeCommRing.of

added theorem FreeCommRing.of_injective

added def FreeCommRing.restriction

added theorem FreeCommRing.restriction_of

added def FreeCommRing

added def FreeRing.castFreeCommRing

added def FreeRing.coeRingHom

added theorem FreeRing.coe_eq

added def FreeRing.subsingletonEquivFreeCommRing

added def FreeRing.toFreeCommRing

added def freeCommRingEquivMvPolynomialInt

added def freeCommRingPemptyEquivInt

added def freeCommRingPunitEquivPolynomialInt

added def freeRingPemptyEquivInt

added def freeRingPunitEquivPolynomialInt