HasseDeriv

📁 Source: Mathlib/Algebra/Polynomial/HasseDeriv.lean

Statistics

Metric	Count
Definitions hasseDeriv	1
Theorems factorial_smul_hasseDeriv, hasseDeriv_C, hasseDeriv_X, hasseDeriv_apply, hasseDeriv_apply_one, hasseDeriv_coeff, hasseDeriv_comp, hasseDeriv_eq_zero_of_lt_natDegree, hasseDeriv_monomial, hasseDeriv_mul, hasseDeriv_natDegree_eq_C, hasseDeriv_one, hasseDeriv_one', hasseDeriv_zero, hasseDeriv_zero', natDegree_hasseDeriv, natDegree_hasseDeriv_le	17
Total	18

Polynomial

Definitions

Name	Category	Theorems
hasseDeriv 📖	CompOp	18 math math: hasseDeriv_zero', hasseDeriv_one', hasseDeriv_comp, natDegree_hasseDeriv_le, hasseDeriv_coeff, hasseDeriv_mul, hasseDeriv_zero, natDegree_hasseDeriv, hasseDeriv_monomial, factorial_smul_hasseDeriv, hasseDeriv_C, hasseDeriv_apply_one, hasseDeriv_natDegree_eq_C, hasseDeriv_apply, taylor_coeff, hasseDeriv_one, hasseDeriv_X, hasseDeriv_eq_zero_of_lt_natDegree

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
factorial_smul_hasseDeriv 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike AddMonoid.toNatSMul AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Module.End.instSemiring Nat.factorial hasseDeriv Nat.iterate derivative	—	hasseDeriv_zero Nat.factorial_zero Function.iterate_zero one_smul LinearMap.id_coe ext Function.iterate_succ_apply' coeff_smul hasseDeriv_coeff LinearMap.map_smul_of_tower LinearMap.IsScalarTower.compatibleSMul AddCommMonoid.nat_isScalarTower coeff_derivative Nat.choose_symm_add nsmul_eq_mul add_right_comm mul_assoc Commute.eq Nat.cast_commute mul_comm add_assoc Nat.choose_symm_of_eq_add Nat.choose_succ_right_eq add_tsub_cancel_left Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid
hasseDeriv_C 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike hasseDeriv RingHom RingHom.instFunLike C instZero	—	monomial_zero_left hasseDeriv_monomial Nat.choose_eq_zero_of_lt Nat.cast_zero MulZeroClass.zero_mul monomial_zero_right
hasseDeriv_X 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike hasseDeriv X instZero	—	monomial_one_one_eq_X hasseDeriv_monomial Nat.choose_eq_zero_of_lt Nat.cast_zero MulZeroClass.zero_mul monomial_zero_right
hasseDeriv_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike hasseDeriv sum monomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Nat.choose	—	nsmul_eq_mul
hasseDeriv_apply_one 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike hasseDeriv instOne instZero	—	C_1 hasseDeriv_C
hasseDeriv_coeff 📖	mathematical	—	coeff DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike hasseDeriv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Nat.choose	—	hasseDeriv_apply coeff_sum sum_def Finset.sum_eq_single coeff_monomial Nat.choose_eq_zero_of_lt Nat.cast_zero MulZeroClass.zero_mul notMem_support_iff MulZeroClass.mul_zero monomial_zero_right add_tsub_cancel_right Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid
hasseDeriv_comp 📖	mathematical	—	LinearMap.comp Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring semiring module Semiring.toModule RingHom.id RingHomCompTriple.ids hasseDeriv LinearMap AddMonoid.toNatSMul AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Module.End.instSemiring Nat.choose	—	lhom_ext' RingHomCompTriple.ids LinearMap.ext_ring hasseDeriv_apply sum_monomial_index MulZeroClass.mul_zero mul_one Nat.instOrderedSub add_comm smul_monomial nsmul_eq_mul Nat.cast_mul Nat.choose_eq_zero_of_lt tsub_lt_iff_right CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le MulZeroClass.zero_mul Nat.cast_injective Rat.instCharZero le_of_add_le_right le_tsub_of_add_le_right le_self_add Nat.cast_choose tsub_add_eq_tsub_tsub add_tsub_cancel_left Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ div_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ one_mul Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero ne_of_gt Nat.cast_pos' Rat.instAddLeftMono Rat.instZeroLEOneClass NeZero.charZero_one Nat.factorial_pos Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat
hasseDeriv_eq_zero_of_lt_natDegree 📖	mathematical	natDegree	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike hasseDeriv instZero	—	hasseDeriv_apply sum_def Finset.sum_eq_zero Nat.choose_eq_zero_of_lt LE.le.trans_lt le_natDegree_of_mem_supp Nat.cast_zero MulZeroClass.zero_mul monomial_zero_right
hasseDeriv_monomial 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike hasseDeriv monomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Nat.choose	—	ext hasseDeriv_coeff coeff_monomial MulZeroClass.mul_zero tsub_eq_iff_eq_add_of_le CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Nat.choose_eq_zero_of_lt Nat.cast_zero MulZeroClass.zero_mul
hasseDeriv_mul 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike hasseDeriv instMul Finset.sum Finset.HasAntidiagonal.antidiagonal Nat.instAddMonoid Finset.Nat.instHasAntidiagonal	—	addHom_ext' AddMonoidHom.ext monomial_mul_monomial hasseDeriv_monomial Finset.sum_congr AddMonoidHom.finset_sum_apply Nat.choose_eq_zero_of_lt Nat.cast_zero MulZeroClass.zero_mul monomial_zero_right MulZeroClass.mul_zero tsub_add_eq_add_tsub CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le add_tsub_assoc_of_le tsub_add_eq_tsub_tsub add_comm mul_assoc Commute.eq Nat.cast_commute Finset.HasAntidiagonal.mem_antidiagonal map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finset.sum_mul Nat.add_choose_eq
hasseDeriv_natDegree_eq_C 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike hasseDeriv natDegree RingHom RingHom.instFunLike C leadingCoeff	—	natDegree_hasseDeriv_le eq_C_of_natDegree_le_zero hasseDeriv_coeff zero_add Nat.choose_self Nat.cast_one one_mul leadingCoeff.eq_1
hasseDeriv_one 📖	mathematical	—	hasseDeriv derivative	—	LinearMap.ext hasseDeriv_one'
hasseDeriv_one' 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike hasseDeriv derivative	—	hasseDeriv_apply Nat.choose_one_right Commute.eq Nat.cast_commute
hasseDeriv_zero 📖	mathematical	—	hasseDeriv LinearMap.id Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring semiring module Semiring.toModule	—	LinearMap.ext hasseDeriv_zero'
hasseDeriv_zero' 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike hasseDeriv	—	hasseDeriv_apply tsub_zero Nat.instOrderedSub Nat.choose_zero_right Nat.cast_one one_mul sum_monomial_eq
natDegree_hasseDeriv 📖	mathematical	—	natDegree DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike hasseDeriv	—	map_natDegree_eq_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass hasseDeriv_eq_zero_of_lt_natDegree hasseDeriv_monomial natDegree_monomial
natDegree_hasseDeriv_le 📖	mathematical	—	natDegree DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike hasseDeriv	—	hasseDeriv_apply sum_def LE.le.trans natDegree_sum_le Finset.fold_congr natDegree_monomial Finset.fold_ite Finset.fold_const max_self max_eq_right Nat.instOrderedSub le_natDegree_of_ne_zero

---

← Back to Index