D

📁 Source: SDG/Basic/D.lean

Statistics

Metric	Count
Definitions D	1
Theorems D_add_sq, D_add_sq_dvd_two, D_mem_mul, D_mul_mem, D_sq, coe_pow, coe_sq, mem_D_add_pow, mem_D_sum_pow, mem_D_sum_pow_succ, mem_𝔻_of_mem_D_add_mem_D, 𝔻_le, 𝔻_mem_mul, 𝔻_mul_mem, 𝔻_pow	15
Total	16

SDG

Definitions

Name	Category	Theorems
D 📖	CompOp	20 math math: taylor_one, D_add_sq, surjective_α, mem_𝔻_of_mem_D_add_mem_D, mem_D_sum_pow, D_eq_𝔻_one, D_mem_iff, D_sq, D_add_sq_dvd_two, mem_D_add_pow, α_apply, zero_mem_D, coe_sq, nontrivial_D, injective_α, bijective_α, derivFun_taylor_one, derivFun_spec, mem_D_sum_pow_succ, derivative_spec

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
D_add_sq 📖	mathematical	—	D	—	𝔻_pow
D_add_sq_dvd_two 📖	mathematical	—	D	—	D_add_sq
D_mem_mul 📖	—	D	—	—	D_mem_iff
D_mul_mem 📖	—	D	—	—	D_mem_iff
D_sq 📖	mathematical	—	D	—	—
coe_pow 📖	mathematical	—	𝔻	—	𝔻_pow
coe_sq 📖	mathematical	—	D	—	—
mem_D_add_pow 📖	mathematical	—	D	—	𝔻_pow
mem_D_sum_pow 📖	mathematical	—	List.Fin.fintype D	—	Fin.sum_univ_succ mem_D_add_pow mem_D_sum_pow_succ Fin.prod_univ_succ
mem_D_sum_pow_succ 📖	mathematical	—	List.Fin.fintype D	—	Fin.sum_univ_succ mem_D_add_pow
mem_𝔻_of_mem_D_add_mem_D 📖	mathematical	—	𝔻 D	—	𝔻_pow
𝔻_le 📖	mathematical	—	𝔻	—	𝔻_mem_iff
𝔻_mem_mul 📖	—	𝔻	—	—	𝔻_mem_iff
𝔻_mul_mem 📖	—	𝔻	—	—	𝔻_mem_iff
𝔻_pow 📖	mathematical	—	𝔻	—	—

---

← Back to Index