ShiftedLegendre

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

Statistics

Metric	Count
Definitions shiftedLegendre	1
Theorems coeff_shiftedLegendre, degree_shiftedLegendre, factorial_mul_shiftedLegendre_eq, natDegree_shiftedLegendre, neg_one_pow_mul_shiftedLegendre_comp_one_sub_X_eq, shiftedLegendre_eval_symm	6
Total	7

Polynomial

Definitions

Name	Category	Theorems
shiftedLegendre 📖	CompOp	6 math math: coeff_shiftedLegendre, factorial_mul_shiftedLegendre_eq, degree_shiftedLegendre, natDegree_shiftedLegendre, shiftedLegendre_eval_symm, neg_one_pow_mul_shiftedLegendre_comp_one_sub_X_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeff_shiftedLegendre 📖	mathematical	—	coeff Int.instSemiring shiftedLegendre Monoid.toNatPow Int.instMonoid Nat.choose	—	shiftedLegendre.eq_1 finset_sum_coeff Finset.sum_congr coeff_C_mul_X_pow Finset.sum_ite_eq Nat.instNoMaxOrder Nat.choose_eq_zero_of_lt CharP.cast_eq_zero CharP.ofCharZero Int.instCharZero MulZeroClass.mul_zero MulZeroClass.zero_mul
degree_shiftedLegendre 📖	mathematical	—	degree Int.instSemiring shiftedLegendre WithBot AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne	—	le_antisymm degree_le_iff_coeff_zero coeff_shiftedLegendre Nat.choose_eq_zero_of_lt WithBot.addLeftMono IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid WithBot.zeroLEOneClass Nat.instZeroLEOneClass WithBot.charZero Nat.instCharZero CharP.cast_eq_zero CharP.ofCharZero Int.instCharZero MulZeroClass.mul_zero MulZeroClass.zero_mul le_degree_of_ne_zero Nat.choose_self Nat.cast_one mul_one IsStrictOrderedRing.noZeroDivisors Int.instIsStrictOrderedRing AddGroup.existsAddOfLE isReduced_of_noZeroDivisors Int.instNontrivial LT.lt.ne' Nat.choose_pos IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Nat.instCanonicallyOrderedAdd
factorial_mul_shiftedLegendre_eq 📖	mathematical	—	Polynomial Int.instSemiring instMul instNatCast Nat.factorial shiftedLegendre Nat.iterate DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike derivative Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero X instSub Int.instRing instOne	—	mul_pow mul_one_sub pow_two sub_eq_add_neg add_comm add_pow Finset.sum_congr neg_pow mul_assoc mul_comm pow_mul_pow_sub le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Int.instIsStrictOrderedRing neg_neg_of_pos Int.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_nonpos_of_le IsStrictOrderedRing.toIsOrderedRing Nat.cast_add Nat.cast_one Finset.mem_range pow_add nsmul_eq_mul iterate_derivative_sum eq_intCast RingHom.instRingHomClass Int.cast_mul Int.cast_natCast Int.cast_pow Int.cast_neg Int.cast_one iterate_derivative_C_mul iterate_derivative_X_pow_eq_smul Nat.descFactorial_eq_div zsmul_eq_mul Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.pow_prod_atom Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow C_mul Nat.add_choose Nat.cast_mul Nat.factorial_pos Finset.mul_sum
natDegree_shiftedLegendre 📖	mathematical	—	natDegree Int.instSemiring shiftedLegendre	—	natDegree_eq_of_degree_eq_some degree_shiftedLegendre
neg_one_pow_mul_shiftedLegendre_comp_one_sub_X_eq 📖	mathematical	—	Polynomial Int.instSemiring instMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring instNeg Int.instRing instOne comp shiftedLegendre instSub X	—	nat_mul_inj' instNoZeroDivisors IsStrictOrderedRing.noZeroDivisors Int.instIsStrictOrderedRing AddGroup.existsAddOfLE charZero Int.instCharZero mul_assoc mul_comm natCast_mul_comp factorial_mul_shiftedLegendre_eq iterate_derivative_comp_one_sub_X mul_comp pow_comp X_comp sub_comp one_comp sub_sub_cancel Nat.factorial_ne_zero
shiftedLegendre_eval_symm 📖	mathematical	—	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring Int.instCommSemiring semiring Ring.toSemiring algebraOfAlgebra Algebra.id Ring.toIntAlgebra AlgHom.funLike aeval shiftedLegendre Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup	—	neg_one_pow_mul_shiftedLegendre_comp_one_sub_X_eq map_mul NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass aeval_neg map_one MonoidHomClass.toOneHomClass aeval_comp aeval_sub aeval_X

---

← Back to Index