Documentation Verification Report

FreeCommRing

📁 Source: Mathlib/RingTheory/MvPolynomial/FreeCommRing.lean

Statistics

Metric	Count
Definitions `genericPolyMap`, `mvPolynomialSupportLEEquiv`, `FreeCommRing`	3
Theorems `MvPolynomialSupportLEEquiv_symm_apply_coeff`, `lift_genericPolyMap`	2
Total	5

FirstOrder.Ring

Definitions

Name	Category	Theorems
`genericPolyMap` 📖	CompOp	1 math math: `lift_genericPolyMap`
`mvPolynomialSupportLEEquiv` 📖	CompOp	2 math math: `lift_genericPolyMap`, `MvPolynomialSupportLEEquiv_symm_apply_coeff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`MvPolynomialSupportLEEquiv_symm_apply_coeff` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `mvPolynomialSupportLEEquiv` `MvPolynomial.support` `CommRing.toCommSemiring` `MvPolynomial.coeff` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.Subset.refl`	—	`Equiv.symm_apply_apply` `Finset.Subset.refl`
`lift_genericPolyMap` 📖	mathematical	—	`DFunLike.coe` `RingHom` `FreeCommRing` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finset` `Finset.instMembership` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRingFreeCommRing` `RingHom.instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `FreeCommRing.lift` `genericPolyMap` `MvPolynomial` `MvPolynomial.commSemiring` `MvPolynomial.eval` `Equiv.symm` `mvPolynomialSupportLEEquiv` `SetLike.instMembership` `Finset.instSetLike`	—	`map_sum` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `Finset.sum_congr` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `FreeCommRing.lift_of` `Finset.filter.congr_simp` `Finset.prod_congr` `Finset.sum_filter` `Finset.sum_attach` `map_prod` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `map_pow` `Subtype.coe_eta` `MulZeroClass.zero_mul`

(root)

Definitions

Name	Category	Theorems
`FreeCommRing` 📖	CompOp	29 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.of_injective`, `instInfiniteFreeCommRing`, `FreeCommRing.isSupported_zero`, `FreeRing.coe_surjective`, `FreeCommRing.isSupported_neg`, `FreeCommRing.isSupported_sub`, `FreeCommRing.restriction_of`, `FreeCommRing.map_of`, `FreeRing.coe_sub`, `FreeCommRing.isSupported_add`, `Cardinal.mk_freeCommRing`, `FreeRing.coe_mul`, `instCountableFreeCommRing`, `FreeCommRing.isSupported_one`, `FreeCommRing.map_subtype_val_restriction`

---

← Back to Index