IntegralNormalization

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

Statistics

Metric	Count
Definitions `integralNormalization`	1
Theorems `degree_integralNormalization`, `integralNormalization_C`, `integralNormalization_aeval_eq_zero`, `integralNormalization_coeff`, `integralNormalization_coeff_degree`, `integralNormalization_coeff_degree_ne`, `integralNormalization_coeff_mul_leadingCoeff_pow`, `integralNormalization_coeff_natDegree`, `integralNormalization_coeff_ne_natDegree`, `integralNormalization_degree`, `integralNormalization_eval₂_eq_zero`, `integralNormalization_eval₂_eq_zero_of_commute`, `integralNormalization_eval₂_leadingCoeff_mul`, `integralNormalization_eval₂_leadingCoeff_mul_of_commute`, `integralNormalization_map`, `integralNormalization_mul_C_leadingCoeff`, `integralNormalization_zero`, `leadingCoeff_smul_integralNormalization`, `monic_integralNormalization`, `natDegree_integralNormalization`, `support_integralNormalization`, `support_integralNormalization_subset`	22
Total	23

Polynomial

Definitions

Name	Category	Theorems
`integralNormalization` 📖	CompOp	23 math math: `integralNormalization_degree`, `integralNormalization_C`, `integralNormalization_coeff_natDegree`, `integralNormalization_aeval_eq_zero`, `leadingCoeff_smul_integralNormalization`, `integralNormalization_map`, `natDegree_integralNormalization`, `monic_integralNormalization`, `integralNormalization_coeff_degree`, `integralNormalization_eval₂_eq_zero`, `degree_integralNormalization`, `support_integralNormalization_subset`, `support_integralNormalization`, `integralNormalization_coeff_mul_leadingCoeff_pow`, `integralNormalization_coeff_degree_ne`, `integralNormalization_mul_C_leadingCoeff`, `integralNormalization_eval₂_leadingCoeff_mul_of_commute`, `integralNormalization_coeff`, `integralNormalization_zero`, `integralNormalization_coeff_ne_natDegree`, `resultant_integralNormalization`, `integralNormalization_eval₂_eq_zero_of_commute`, `integralNormalization_eval₂_leadingCoeff_mul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`degree_integralNormalization` 📖	mathematical	—	`degree` `integralNormalization`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `degree_of_subsingleton` `integralNormalization_zero` `degree_eq_natDegree` `degree_eq_of_le_of_coeff_ne_zero` `Finset.sup_le` `WithBot.coe_le_coe` `le_natDegree_of_mem_supp` `support_integralNormalization_subset` `integralNormalization_coeff_natDegree` `NeZero.one`
`integralNormalization_C` 📖	mathematical	—	`integralNormalization` `DFunLike.coe` `RingHom` `Polynomial` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `instOne`	—	`degree_C` `leadingCoeff_C` `natDegree_C` `zero_tsub` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `pow_zero` `mul_one` `Finset.sum_congr` `support_C` `Finset.sum_singleton` `CharP.cast_eq_zero` `CharP.ofCharZero` `WithBot.charZero` `Nat.instCharZero` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`integralNormalization_aeval_eq_zero` 📖	mathematical	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `aeval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `RingHom` `RingHom.instFunLike` `algebraMap` `leadingCoeff` `integralNormalization`	—	`integralNormalization_eval₂_eq_zero_of_commute` `Algebra.commute_algebraMap_left` `Commute.map` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `Commute.all`
`integralNormalization_coeff` 📖	mathematical	—	`coeff` `integralNormalization` `WithBot` `degree` `AddMonoidWithOne.toNatCast` `WithBot.addMonoidWithOne` `Nat.instAddMonoidWithOne` `WithBot.decidableEq` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `leadingCoeff` `natDegree`	—	`coeff_ne_zero_of_eq_degree` `finset_sum_coeff` `Finset.sum_congr` `coeff_monomial` `Finset.sum_ite_eq'` `MulZeroClass.zero_mul`
`integralNormalization_coeff_degree` 📖	mathematical	`degree` `WithBot` `AddMonoidWithOne.toNatCast` `WithBot.addMonoidWithOne` `Nat.instAddMonoidWithOne`	`coeff` `integralNormalization` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	`integralNormalization_coeff`
`integralNormalization_coeff_degree_ne` 📖	mathematical	—	`coeff` `integralNormalization` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `leadingCoeff` `natDegree`	—	`integralNormalization_coeff`
`integralNormalization_coeff_mul_leadingCoeff_pow` 📖	mathematical	`natDegree`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `coeff` `integralNormalization` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `leadingCoeff`	—	`integralNormalization_coeff` `natDegree_eq_of_degree_eq_some` `one_mul` `tsub_add_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `mul_assoc` `le_tsub_iff_right` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `coe_lt_degree` `coeff_eq_zero_of_degree_lt` `lt_of_le_of_ne` `le_of_not_gt` `MulZeroClass.zero_mul`
`integralNormalization_coeff_natDegree` 📖	mathematical	—	`coeff` `integralNormalization` `natDegree` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	`integralNormalization_coeff_degree` `degree_eq_natDegree`
`integralNormalization_coeff_ne_natDegree` 📖	mathematical	—	`coeff` `integralNormalization` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `leadingCoeff` `natDegree`	—	`integralNormalization_coeff_degree_ne` `degree_ne_of_natDegree_ne`
`integralNormalization_degree` 📖	mathematical	—	`degree` `integralNormalization`	—	`degree_integralNormalization`
`integralNormalization_eval₂_eq_zero` 📖	mathematical	`eval₂` `CommSemiring.toSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `leadingCoeff` `integralNormalization`	—	`integralNormalization_eval₂_eq_zero_of_commute` `Commute.all`
`integralNormalization_eval₂_eq_zero_of_commute` 📖	mathematical	`eval₂` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `leadingCoeff`	`integralNormalization`	—	`eq_C_of_natDegree_eq_zero` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `MulZeroClass.zero_mul` `integralNormalization_zero` `eval₂_zero` `eval₂_C` `integralNormalization_eval₂_leadingCoeff_mul_of_commute` `MulZeroClass.mul_zero`
`integralNormalization_eval₂_leadingCoeff_mul` 📖	mathematical	`natDegree`	`eval₂` `CommSemiring.toSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `leadingCoeff` `integralNormalization` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`integralNormalization_eval₂_leadingCoeff_mul_of_commute` `Commute.all`
`integralNormalization_eval₂_leadingCoeff_mul_of_commute` 📖	mathematical	`natDegree` `Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `leadingCoeff`	`eval₂` `integralNormalization` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`eval₂_eq_sum_range` `Finset.mul_sum` `Finset.sum_congr` `natDegree_eq_of_degree_eq` `degree_integralNormalization` `Commute.mul_pow` `mul_assoc` `RingHom.map_pow` `RingHom.map_mul` `integralNormalization_coeff_mul_leadingCoeff_pow` `Commute.eq`
`integralNormalization_map` 📖	mathematical	—	`integralNormalization` `map`	—	`ext` `integralNormalization_coeff` `degree_map_eq_of_leadingCoeff_ne_zero` `coeff_map` `leadingCoeff_map_of_leadingCoeff_ne_zero` `natDegree_map_eq_iff` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `map_pow`
`integralNormalization_mul_C_leadingCoeff` 📖	mathematical	—	`Polynomial` `instMul` `integralNormalization` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `leadingCoeff` `scaleRoots`	—	`ext` `coeff_mul_C` `integralNormalization_coeff` `natDegree_eq_of_degree_eq_some` `one_mul` `coeff_scaleRoots` `tsub_self` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `pow_zero` `mul_one` `mul_assoc` `pow_succ` `tsub_right_comm` `tsub_add_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `le_tsub_iff_left` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `LT.lt.le` `coe_lt_degree` `coeff_eq_zero_of_degree_lt` `lt_of_le_of_ne` `le_of_not_gt` `MulZeroClass.zero_mul`
`integralNormalization_zero` 📖	mathematical	—	`integralNormalization` `Polynomial` `instZero`	—	`zero_tsub` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `pow_zero` `mul_one` `sum_zero_index`
`leadingCoeff_smul_integralNormalization` 📖	mathematical	—	`Polynomial` `CommSemiring.toSemiring` `Algebra.toSMul` `semiring` `algebraOfAlgebra` `Algebra.id` `leadingCoeff` `integralNormalization` `scaleRoots`	—	`Algebra.smul_def` `algebraMap_eq` `mul_comm` `integralNormalization_mul_C_leadingCoeff`
`monic_integralNormalization` 📖	mathematical	—	`Monic` `integralNormalization`	—	`monic_of_degree_le` `Finset.sup_le` `WithBot.coe_le_coe` `le_natDegree_of_mem_supp` `support_integralNormalization_subset` `integralNormalization_coeff_natDegree`
`natDegree_integralNormalization` 📖	mathematical	—	`natDegree` `integralNormalization`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `natDegree_of_subsingleton` `integralNormalization_zero` `natDegree_eq_of_degree_eq` `degree_integralNormalization`
`support_integralNormalization` 📖	mathematical	—	`support` `integralNormalization`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `Subsingleton.eq_zero` `Unique.instSubsingleton` `integralNormalization_zero` `Finset.ext` `support_integralNormalization_subset` `integralNormalization_coeff` `NeZero.one` `IsDomain.to_noZeroDivisors` `isReduced_of_noZeroDivisors`
`support_integralNormalization_subset` 📖	mathematical	—	`Finset` `Finset.instHasSubset` `support` `integralNormalization`	—	`finset_sum_coeff` `Finset.sum_congr` `coeff_monomial` `Finset.sum_ite_eq'`

---

← Back to Index