Documentation Verification Report

Opposites

📁 Source: Mathlib/RingTheory/Polynomial/Opposites.lean

Statistics

Metric	Count
Definitions `opRingEquiv`	1
Theorems `coeff_opRingEquiv`, `isCancelMulZero_iff`, `isDomain_iff`, `isLeftCancelMulZero_iff`, `isRightCancelMulZero_iff`, `leadingCoeff_opRingEquiv`, `natDegree_opRingEquiv`, `opRingEquiv_op_C`, `opRingEquiv_op_C_mul_X_pow`, `opRingEquiv_op_X`, `opRingEquiv_op_monomial`, `opRingEquiv_symm_C`, `opRingEquiv_symm_C_mul_X_pow`, `opRingEquiv_symm_X`, `opRingEquiv_symm_monomial`, `support_opRingEquiv`	16
Total	17

Polynomial

Definitions

Name	Category	Theorems
`opRingEquiv` 📖	CompOp	12 math math: `opRingEquiv_op_monomial`, `leadingCoeff_opRingEquiv`, `opRingEquiv_op_C`, `opRingEquiv_op_X`, `opRingEquiv_symm_C_mul_X_pow`, `opRingEquiv_symm_monomial`, `support_opRingEquiv`, `coeff_opRingEquiv`, `opRingEquiv_symm_C`, `natDegree_opRingEquiv`, `opRingEquiv_op_C_mul_X_pow`, `opRingEquiv_symm_X`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeff_opRingEquiv` 📖	mathematical	—	`coeff` `MulOpposite` `MulOpposite.instSemiring` `DFunLike.coe` `RingEquiv` `Polynomial` `MulOpposite.instMul` `instMul` `MulOpposite.instAdd` `instAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `opRingEquiv` `MulOpposite.op` `MulOpposite.unop`	—	`AddMonoidAlgebra.mapDomainRingEquiv_apply`
`isCancelMulZero_iff` 📖	mathematical	—	`IsCancelMulZero` `Polynomial` `instMul` `instZero` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `IsCancelAdd` `Distrib.toAdd`	—	—
`isDomain_iff` 📖	mathematical	—	`IsDomain` `Polynomial` `semiring` `IsCancelAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	—
`isLeftCancelMulZero_iff` 📖	mathematical	—	`IsLeftCancelMulZero` `Polynomial` `instMul` `instZero` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `IsCancelAdd` `Distrib.toAdd`	—	`Function.Injective.isLeftCancelMulZero` `C_injective` `C_0` `C_mul` `Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `mul_add` `Distrib.leftDistribClass` `add_mul` `Distrib.rightDistribClass` `X_mul_C` `one_mul` `C_add` `pow_succ` `pow_zero` `mul_assoc` `Mathlib.Tactic.Abel.subst_into_add` `Mathlib.Tactic.Abel.term_atom` `Mathlib.Tactic.Abel.term_add_const` `zero_add` `Mathlib.Tactic.Abel.const_add_term` `add_zero` `coeff_add` `coeff_smul` `coeff_X_pow` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `MulZeroClass.mul_zero` `coeff_X_one` `mul_one` `coeff_C_succ` `IsLeftCancelMulZero.mul_left_cancel_of_ne_zero` `X_add_C_ne_zero` `AddCommMagma.IsLeftCancelAdd.toIsCancelAdd` `instIsLeftCancelMulZeroOfIsCancelAdd`
`isRightCancelMulZero_iff` 📖	mathematical	—	`IsRightCancelMulZero` `Polynomial` `instMul` `instZero` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `IsCancelAdd` `Distrib.toAdd`	—	`MulOpposite.isLeftCancelMulZero_iff` `MulEquiv.isLeftCancelMulZero_iff` `isLeftCancelMulZero_iff` `MulOpposite.isCancelAdd_iff`
`leadingCoeff_opRingEquiv` 📖	mathematical	—	`leadingCoeff` `MulOpposite` `MulOpposite.instSemiring` `DFunLike.coe` `RingEquiv` `Polynomial` `MulOpposite.instMul` `instMul` `MulOpposite.instAdd` `instAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `opRingEquiv` `MulOpposite.op` `MulOpposite.unop`	—	`leadingCoeff.eq_1` `coeff_opRingEquiv` `natDegree_opRingEquiv`
`natDegree_opRingEquiv` 📖	mathematical	—	`natDegree` `MulOpposite` `MulOpposite.instSemiring` `DFunLike.coe` `RingEquiv` `Polynomial` `MulOpposite.instMul` `instMul` `MulOpposite.instAdd` `instAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `opRingEquiv` `MulOpposite.unop`	—	`map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `nonempty_support_iff` `EquivLike.toEmbeddingLike` `support_opRingEquiv` `natDegree_eq_support_max'` `Finset.max'.congr_simp`
`opRingEquiv_op_C` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `MulOpposite` `Polynomial` `MulOpposite.instSemiring` `MulOpposite.instMul` `instMul` `MulOpposite.instAdd` `instAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `opRingEquiv` `MulOpposite.op` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C`	—	`opRingEquiv_op_monomial`
`opRingEquiv_op_C_mul_X_pow` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `MulOpposite` `Polynomial` `MulOpposite.instSemiring` `MulOpposite.instMul` `instMul` `MulOpposite.instAdd` `instAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `opRingEquiv` `MulOpposite.op` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X`	—	`map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingEquivClass.toNonUnitalRingHomClass` `RingEquiv.instRingEquivClass` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingEquivClass.toRingHomClass` `opRingEquiv_op_X` `opRingEquiv_op_C` `X_pow_mul`
`opRingEquiv_op_X` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `MulOpposite` `Polynomial` `MulOpposite.instSemiring` `MulOpposite.instMul` `instMul` `MulOpposite.instAdd` `instAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `opRingEquiv` `MulOpposite.op` `X`	—	`opRingEquiv_op_monomial`
`opRingEquiv_op_monomial` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `MulOpposite` `Polynomial` `MulOpposite.instSemiring` `MulOpposite.instMul` `instMul` `MulOpposite.instAdd` `instAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `opRingEquiv` `MulOpposite.op` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `semiring` `Semiring.toModule` `module` `LinearMap.instFunLike` `monomial`	—	`toFinsupp_monomial` `Finsupp.mapRange_single` `Finsupp.equivMapDomain_single` `AddMonoidAlgebra.mapDomainRingEquiv_single` `ofFinsupp_single`
`opRingEquiv_symm_C` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `Polynomial` `MulOpposite` `MulOpposite.instSemiring` `instMul` `MulOpposite.instMul` `instAdd` `MulOpposite.instAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `opRingEquiv` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `MulOpposite.op` `MulOpposite.unop`	—	`opRingEquiv_symm_monomial`
`opRingEquiv_symm_C_mul_X_pow` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `Polynomial` `MulOpposite` `MulOpposite.instSemiring` `instMul` `MulOpposite.instMul` `instAdd` `MulOpposite.instAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `opRingEquiv` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X` `MulOpposite.op` `MulOpposite.unop`	—	`C_mul_X_pow_eq_monomial` `opRingEquiv_symm_monomial`
`opRingEquiv_symm_X` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `Polynomial` `MulOpposite` `MulOpposite.instSemiring` `instMul` `MulOpposite.instMul` `instAdd` `MulOpposite.instAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `opRingEquiv` `X` `MulOpposite.op`	—	`opRingEquiv_symm_monomial`
`opRingEquiv_symm_monomial` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `Polynomial` `MulOpposite` `MulOpposite.instSemiring` `instMul` `MulOpposite.instMul` `instAdd` `MulOpposite.instAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `opRingEquiv` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `semiring` `Semiring.toModule` `module` `LinearMap.instFunLike` `monomial` `MulOpposite.op` `MulOpposite.unop`	—	`RingEquiv.injective` `RingEquiv.apply_symm_apply` `opRingEquiv_op_monomial`
`support_opRingEquiv` 📖	mathematical	—	`support` `MulOpposite` `MulOpposite.instSemiring` `DFunLike.coe` `RingEquiv` `Polynomial` `MulOpposite.instMul` `instMul` `MulOpposite.instAdd` `instAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `opRingEquiv` `MulOpposite.unop`	—	`Finset.ext` `coeff_opRingEquiv`

---

← Back to Index