FreeCommRing

📁 Source: Mathlib/RingTheory/FreeCommRing.lean

Statistics

Metric	Count
Definitions `map`, `of`, `restriction`, `instCoe`, `castFreeCommRing`, `coeRingHom`, `instCommRing`, `subsingletonEquivFreeCommRing`, `toFreeCommRing`, `freeCommRingEquivMvPolynomialInt`, `freeCommRingPEmptyEquivInt`, `freeCommRingPUnitEquivPolynomialInt`, `freeCommRingPemptyEquivInt`, `freeCommRingPunitEquivPolynomialInt`, `freeRingPEmptyEquivInt`, `freeRingPUnitEquivPolynomialInt`, `freeRingPemptyEquivInt`, `freeRingPunitEquivPolynomialInt`, `instCommRingFreeCommRing`, `instInhabitedFreeCommRing`	20
Theorems `exists_finite_support`, `exists_finset_support`, `hom_ext`, `hom_ext_iff`, `induction_on`, `isSupported_add`, `isSupported_int`, `isSupported_mul`, `isSupported_neg`, `isSupported_of`, `isSupported_one`, `isSupported_sub`, `isSupported_upwards`, `isSupported_zero`, `lift_comp_of`, `lift_of`, `map_of`, `map_subtype_val_restriction`, `of_cons`, `of_injective`, `of_ne_one`, `of_ne_zero`, `one_ne_of`, `restriction_of`, `zero_ne_of`, `coe_add`, `coe_eq`, `coe_mul`, `coe_neg`, `coe_of`, `coe_one`, `coe_sub`, `coe_surjective`, `coe_zero`	34
Total	54

FreeCommRing

Definitions

Name	Category	Theorems
`map` 📖	CompOp	2 math math: `map_of`, `map_subtype_val_restriction`
`of` 📖	CompOp	10 math math: `isSupported_of`, `lift_of`, `hom_ext_iff`, `FreeRing.coe_of`, `lift_comp_of`, `of_cons`, `Ring.DirectLimit.quotientMk_of`, `of_injective`, `restriction_of`, `map_of`
`restriction` 📖	CompOp	2 math math: `restriction_of`, `map_subtype_val_restriction`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_finite_support` 📖	mathematical	—	`Set.Finite` `IsSupported`	—	`induction_on` `Set.finite_empty` `isSupported_neg` `isSupported_one` `Set.finite_singleton` `isSupported_of` `Set.mem_singleton` `Set.Finite.union` `isSupported_add` `isSupported_upwards` `Set.subset_union_left` `Set.subset_union_right` `isSupported_mul`
`exists_finset_support` 📖	mathematical	—	`IsSupported` `SetLike.coe` `Finset` `Finset.instSetLike`	—	`exists_finite_support` `Set.Finite.coe_toFinset`
`hom_ext` 📖	—	`DFunLike.coe` `RingHom` `FreeCommRing` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRingFreeCommRing` `RingHom.instFunLike` `of`	—	—	`Equiv.injective`
`hom_ext_iff` 📖	mathematical	—	`DFunLike.coe` `RingHom` `FreeCommRing` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRingFreeCommRing` `RingHom.instFunLike` `of`	—	`hom_ext`
`induction_on` 📖	—	`FreeCommRing` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `instCommRingFreeCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `of` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toMul`	—	—	`neg_one_mul` `neg_neg` `FreeAbelianGroup.induction_on` `neg_add_cancel` `Multiset.induction_on`
`isSupported_add` 📖	mathematical	`IsSupported`	`FreeCommRing` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRingFreeCommRing`	—	`Subring.add_mem`
`isSupported_int` 📖	mathematical	—	`IsSupported` `FreeCommRing` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `CommRing.toRing` `instCommRingFreeCommRing`	—	`Int.induction_on` `isSupported_zero` `Int.cast_add` `Int.cast_one` `isSupported_add` `isSupported_one` `Int.cast_sub` `isSupported_sub`
`isSupported_mul` 📖	mathematical	`IsSupported`	`FreeCommRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRingFreeCommRing`	—	`Subring.mul_mem`
`isSupported_neg` 📖	mathematical	`IsSupported`	`FreeCommRing` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `instCommRingFreeCommRing`	—	`Subring.neg_mem`
`isSupported_of` 📖	mathematical	—	`IsSupported` `of` `Set` `Set.instMembership`	—	`map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Nat.cast_one` `Int.cast_one` `Polynomial.charZero` `Int.instCharZero` `map_neg` `RingHomClass.toAddMonoidHomClass` `Int.cast_neg` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `lift_of` `MulZeroClass.zero_mul` `Nat.cast_zero` `Int.cast_zero` `map_add` `AddMonoidHomClass.toAddHomClass` `Polynomial.C_eq_intCast` `Polynomial.coeff_X` `one_ne_zero` `Polynomial.coeff_C` `Subring.subset_closure`
`isSupported_one` 📖	mathematical	—	`IsSupported` `FreeCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `instCommRingFreeCommRing`	—	`Subring.one_mem`
`isSupported_sub` 📖	mathematical	`IsSupported`	`FreeCommRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `instCommRingFreeCommRing`	—	`Subring.sub_mem`
`isSupported_upwards` 📖	—	`IsSupported` `Set` `Set.instHasSubset`	—	—	`Subring.closure_mono` `Set.monotone_image`
`isSupported_zero` 📖	mathematical	—	`IsSupported` `FreeCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRingFreeCommRing`	—	`Subring.zero_mem`
`lift_comp_of` 📖	mathematical	—	`DFunLike.coe` `Equiv` `RingHom` `FreeCommRing` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRingFreeCommRing` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `RingHom.instFunLike` `of`	—	`RingHom.ext` `induction_on` `map_neg` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.map_neg` `RingHom.map_one` `lift_of` `map_add` `AddMonoidHomClass.toAddHomClass` `RingHom.map_add` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.map_mul`
`lift_of` 📖	mathematical	—	`DFunLike.coe` `RingHom` `FreeCommRing` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRingFreeCommRing` `RingHom.instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `of`	—	`FreeAbelianGroup.lift_apply_of` `mul_one`
`map_of` 📖	mathematical	—	`DFunLike.coe` `RingHom` `FreeCommRing` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRingFreeCommRing` `RingHom.instFunLike` `map` `of`	—	`lift_of`
`map_subtype_val_restriction` 📖	mathematical	`IsSupported`	`DFunLike.coe` `RingHom` `FreeCommRing` `Set.Elem` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRingFreeCommRing` `RingHom.instFunLike` `map` `Set` `Set.instMembership` `restriction`	—	`map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `map_neg` `RingHomClass.toAddMonoidHomClass` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `restriction_of` `map_of` `map_add` `AddMonoidHomClass.toAddHomClass`
`of_cons` 📖	mathematical	—	`FreeAbelianGroup.of` `Multiplicative` `Multiset` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Multiplicative.ofAdd` `Multiset.cons` `FreeCommRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRingFreeCommRing` `of`	—	`Multiset.singleton_add` `ofAdd_add` `of.eq_1` `FreeAbelianGroup.of_mul_of`
`of_injective` 📖	mathematical	—	`FreeCommRing` `of`	—	`FreeAbelianGroup.of_injective` `Multiset.coe_eq_coe`
`of_ne_one` 📖	—	—	—	—	`FreeAbelianGroup.of_injective` `Multiset.singleton_ne_zero`
`of_ne_zero` 📖	—	—	—	—	`FreeAbelianGroup.of_ne_zero`
`one_ne_of` 📖	—	—	—	—	`FreeAbelianGroup.of_injective` `Multiset.zero_ne_singleton`
`restriction_of` 📖	mathematical	—	`DFunLike.coe` `RingHom` `FreeCommRing` `Set.Elem` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRingFreeCommRing` `RingHom.instFunLike` `restriction` `of` `Set` `Set.instMembership` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`lift_of`
`zero_ne_of` 📖	—	—	—	—	`FreeAbelianGroup.zero_ne_of`

FreeRing

Definitions

Name	Category	Theorems
`castFreeCommRing` 📖	CompOp	9 math math: `coe_one`, `coe_neg`, `coe_zero`, `coe_of`, `coe_add`, `coe_surjective`, `coe_sub`, `coe_eq`, `coe_mul`
`coeRingHom` 📖	CompOp	—
`instCommRing` 📖	CompOp	—
`subsingletonEquivFreeCommRing` 📖	CompOp	—
`toFreeCommRing` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_add` 📖	mathematical	—	`castFreeCommRing` `FreeRing` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingFreeRing` `FreeCommRing` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRingFreeCommRing`	—	`RingHom.map_add`
`coe_eq` 📖	mathematical	—	`castFreeCommRing` `FreeAbelianGroup` `FreeAbelianGroup.instMonad` `Multiset` `Multiset.ofList`	—	`AddMonoidHom.instAddMonoidHomClass` `AddMonoidHom.coe_coe` `FreeAbelianGroup.lift_unique` `FreeAbelianGroup.lift_apply_of` `MonoidHom.map_mul` `FreeMonoid.lift_eval_of`
`coe_mul` 📖	mathematical	—	`castFreeCommRing` `FreeRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingFreeRing` `FreeCommRing` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRingFreeCommRing`	—	`RingHom.map_mul`
`coe_neg` 📖	mathematical	—	`castFreeCommRing` `FreeRing` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `instRingFreeRing` `FreeCommRing` `CommRing.toRing` `instCommRingFreeCommRing`	—	`castFreeCommRing.eq_1` `map_neg` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass`
`coe_of` 📖	mathematical	—	`castFreeCommRing` `of` `FreeCommRing.of`	—	`lift_of`
`coe_one` 📖	mathematical	—	`castFreeCommRing` `FreeRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `instRingFreeRing` `FreeCommRing` `CommRing.toRing` `instCommRingFreeCommRing`	—	—
`coe_sub` 📖	mathematical	—	`castFreeCommRing` `FreeRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `instRingFreeRing` `FreeCommRing` `CommRing.toRing` `instCommRingFreeCommRing`	—	`castFreeCommRing.eq_1` `map_sub` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass`
`coe_surjective` 📖	mathematical	—	`FreeRing` `FreeCommRing` `castFreeCommRing`	—	`FreeCommRing.induction_on` `RingHom.map_add` `RingHom.map_mul`
`coe_zero` 📖	mathematical	—	`castFreeCommRing` `FreeRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingFreeRing` `FreeCommRing` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRingFreeCommRing`	—	—

FreeRing.FreeCommRing

Definitions

Name	Category	Theorems
`instCoe` 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
`freeCommRingEquivMvPolynomialInt` 📖	CompOp	—
`freeCommRingPEmptyEquivInt` 📖	CompOp	—
`freeCommRingPUnitEquivPolynomialInt` 📖	CompOp	—
`freeCommRingPemptyEquivInt` 📖	CompOp	—
`freeCommRingPunitEquivPolynomialInt` 📖	CompOp	—
`freeRingPEmptyEquivInt` 📖	CompOp	—
`freeRingPUnitEquivPolynomialInt` 📖	CompOp	—
`freeRingPemptyEquivInt` 📖	CompOp	—
`freeRingPunitEquivPolynomialInt` 📖	CompOp	—
`instCommRingFreeCommRing` 📖	CompOp	24 math math: `FreeCommRing.isSupported_int`, `FreeCommRing.isSupported_mul`, `FreeRing.coe_one`, `FirstOrder.Ring.lift_genericPolyMap`, `FirstOrder.Ring.realize_termOfFreeCommRing`, `FirstOrder.Field.lift_genericMonicPoly`, `FreeRing.coe_neg`, `FreeCommRing.lift_of`, `FreeRing.coe_zero`, `FreeCommRing.hom_ext_iff`, `FreeRing.coe_add`, `FreeCommRing.lift_comp_of`, `FreeCommRing.of_cons`, `Ring.DirectLimit.quotientMk_of`, `FreeCommRing.isSupported_zero`, `FreeCommRing.isSupported_neg`, `FreeCommRing.isSupported_sub`, `FreeCommRing.restriction_of`, `FreeCommRing.map_of`, `FreeRing.coe_sub`, `FreeCommRing.isSupported_add`, `FreeRing.coe_mul`, `FreeCommRing.isSupported_one`, `FreeCommRing.map_subtype_val_restriction`
`instInhabitedFreeCommRing` 📖	CompOp	—

---

← Back to Index