Basic

📁 Source: Mathlib/RingTheory/Polynomial/Hermite/Basic.lean

Statistics

Metric	Count
Definitions hermite	1
Theorems coeff_hermite, coeff_hermite_explicit, coeff_hermite_of_even_add, coeff_hermite_of_lt, coeff_hermite_of_odd_add, coeff_hermite_self, coeff_hermite_succ_succ, coeff_hermite_succ_zero, degree_hermite, hermite_eq_iterate, hermite_monic, hermite_one, hermite_succ, hermite_zero, leadingCoeff_hermite, natDegree_hermite	16
Total	17

Polynomial

Definitions

Name	Category	Theorems
hermite 📖	CompOp	19 math math: natDegree_hermite, coeff_hermite_succ_zero, coeff_hermite_succ_succ, leadingCoeff_hermite, hermite_succ, hermite_eq_iterate, degree_hermite, coeff_hermite_explicit, coeff_hermite_self, hermite_eq_deriv_gaussian', coeff_hermite_of_even_add, deriv_gaussian_eq_hermite_mul_gaussian, hermite_eq_deriv_gaussian, coeff_hermite_of_odd_add, coeff_hermite, hermite_zero, coeff_hermite_of_lt, hermite_monic, hermite_one

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeff_hermite 📖	mathematical	—	coeff Int.instSemiring hermite Even Nat.instDecidablePredEven Monoid.toNatPow Int.instMonoid Nat.doubleFactorial Nat.choose	—	coeff_hermite_of_even_add coeff_hermite_of_odd_add Nat.not_even_iff_odd
coeff_hermite_explicit 📖	mathematical	—	coeff Int.instSemiring hermite Monoid.toNatPow Int.instMonoid Nat.doubleFactorial Nat.choose	—	—
coeff_hermite_of_even_add 📖	mathematical	Even	coeff Int.instSemiring hermite Monoid.toNatPow Int.instMonoid Nat.doubleFactorial Nat.choose	—	le_or_gt Nat.even_sub Nat.even_add coeff_hermite_explicit coeff_hermite_of_lt Nat.choose_eq_zero_of_lt CharP.cast_eq_zero CharP.ofCharZero Int.instCharZero MulZeroClass.mul_zero
coeff_hermite_of_lt 📖	mathematical	—	coeff Int.instSemiring hermite	—	coeff_C Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw coeff_hermite_succ_succ add_right_comm MulZeroClass.mul_zero sub_zero
coeff_hermite_of_odd_add 📖	mathematical	Odd Nat.instSemiring	coeff Int.instSemiring hermite	—	coeff_hermite_of_lt Odd.pos Nat.instCanonicallyOrderedAdd Nat.instNontrivial zero_add coeff_hermite_succ_zero neg_zero coeff_hermite_succ_succ Nat.odd_add even_two MulZeroClass.mul_zero sub_zero
coeff_hermite_self 📖	mathematical	—	coeff Int.instSemiring hermite	—	coeff_C coeff_hermite_succ_succ coeff_hermite_of_lt IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid contravariant_lt_of_covariant_le IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial Nat.instAtLeastTwoHAddOfNat MulZeroClass.mul_zero sub_zero
coeff_hermite_succ_succ 📖	mathematical	—	coeff Int.instSemiring hermite	—	hermite_succ coeff_sub coeff_X_mul coeff_derivative mul_comm Nat.cast_one
coeff_hermite_succ_zero 📖	mathematical	—	coeff Int.instSemiring hermite	—	hermite_succ coeff_sub mul_coeff_zero coeff_X_zero MulZeroClass.zero_mul coeff_derivative zero_add CharP.cast_eq_zero CharP.ofCharZero Int.instCharZero mul_one zero_sub
degree_hermite 📖	mathematical	—	degree Int.instSemiring hermite WithBot AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne	—	degree_eq_of_le_of_coeff_ne_zero WithBot.addLeftMono IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid WithBot.zeroLEOneClass Nat.instZeroLEOneClass WithBot.charZero Nat.instCharZero coeff_hermite_of_lt coeff_hermite_self
hermite_eq_iterate 📖	mathematical	—	hermite Nat.iterate Polynomial Int.instSemiring instSub Int.instRing instMul X DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike derivative instOne	—	Function.iterate_succ_apply' hermite_succ
hermite_monic 📖	mathematical	—	Monic Int.instSemiring hermite	—	leadingCoeff_hermite
hermite_one 📖	mathematical	—	hermite X Int.instSemiring	—	hermite_succ hermite_zero map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass mul_one derivative_one sub_zero
hermite_succ 📖	mathematical	—	hermite Polynomial Int.instSemiring instSub Int.instRing instMul X DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike derivative	—	hermite.eq_2
hermite_zero 📖	mathematical	—	hermite DFunLike.coe RingHom Polynomial Int.instSemiring Semiring.toNonAssocSemiring semiring RingHom.instFunLike C	—	—
leadingCoeff_hermite 📖	mathematical	—	leadingCoeff Int.instSemiring hermite	—	coeff_natDegree natDegree_hermite coeff_hermite_self
natDegree_hermite 📖	mathematical	—	natDegree Int.instSemiring hermite	—	natDegree_eq_of_degree_eq_some degree_hermite

---

← Back to Index