Monad

📁 Source: Mathlib/Algebra/MvPolynomial/Monad.lean

Statistics

Metric	Count
Definitions bind₁, bind₂, join₁, join₂, monad	5
Theorems aeval_bind₁, aeval_bind₂, aeval_comp_bind₁, aeval_eq_bind₁, aeval_id_eq_join₁, aeval_id_rename, bind₁_C_right, bind₁_X_left, bind₁_X_right, bind₁_bind₁, bind₁_comp_bind₁, bind₁_comp_rename, bind₁_id, bind₁_monomial, bind₁_rename, bind₂_C_left, bind₂_C_right, bind₂_X_right, bind₂_bind₂, bind₂_comp_C, bind₂_comp_bind₂, bind₂_id, bind₂_map, bind₂_monomial, bind₂_monomial_one, eval₂Hom_C_eq_bind₁, eval₂Hom_C_id_eq_join₁, eval₂Hom_C_left, eval₂Hom_bind₁, eval₂Hom_bind₂, eval₂Hom_comp_C, eval₂Hom_comp_bind₂, eval₂Hom_eq_bind₂, eval₂Hom_id_X_eq_join₂, hom_bind₁, join₁_rename, join₂_comp_map, join₂_map, lawfulFunctor, lawfulMonad, map_bind₁, map_bind₂, map_comp_C, mem_vars_bind₁, rename_bind₁, rename_comp_bind₁, vars_bind₁	47
Total	52

MvPolynomial

Definitions

Name	Category	Theorems
bind₁ 📖	CompOp	40 math math: join₁_rename, WittVector.bind₁_frobeniusPoly_wittPolynomial, map_bind₁, bind₁_xInTermsOfW_wittPolynomial, eval₂Hom_C_eq_bind₁, bind₁_X_left, bind₁_comp_bind₁, aeval_bind₁, bind₁_C_right, WittVector.bind₁_wittMulN_wittPolynomial, bind₁_rename, wittStructureRat_prop, wittStructureRat_rec, wittStructureRat_rec_aux, wittStructureInt_prop, expand_bind₁, LinearMap.polyCharpoly_eq_of_basis, bind₁_comp_rename, rename_bind₁, bind₁_rename_expand_wittPolynomial, aeval_eq_bind₁, expand_comp_bind₁, aeval_comp_bind₁, LinearMap.toMvPolynomial_comp, vars_bind₁, WittVector.bind₁_verschiebungPoly_wittPolynomial, bind₁_bind₁, WittVector.bind₁_onePoly_wittPolynomial, WittVector.bind₁_zero_wittPolynomial, rename_comp_bind₁, bind₁_wittPolynomial_xInTermsOfW, WittVector.bind₁_frobeniusPolyRat_wittPolynomial, eval₂Hom_bind₁, bind₁_X_right, eval₂Hom_C_left, Matrix.toMvPolynomial_mul, C_p_pow_dvd_bind₁_rename_wittPolynomial_sub_sum, hom_bind₁, bind₁_monomial, bind₁_id
bind₂ 📖	CompOp	17 math math: bind₂_comp_C, bind₂_C_left, map_bind₂, join₂_comp_map, eval₂Hom_comp_bind₂, bind₂_map, bind₂_monomial, bind₂_monomial_one, bind₂_id, bind₂_X_right, aeval_bind₂, bind₂_C_right, eval₂Hom_eq_bind₂, bind₂_comp_bind₂, eval₂Hom_bind₂, bind₂_bind₂, join₂_map
join₁ 📖	CompOp	4 math math: join₁_rename, eval₂Hom_C_id_eq_join₁, aeval_id_eq_join₁, bind₁_id
join₂ 📖	CompOp	4 math math: join₂_comp_map, bind₂_id, eval₂Hom_id_X_eq_join₂, join₂_map
monad 📖	CompOp	2 math math: lawfulFunctor, lawfulMonad

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aeval_bind₁ 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike aeval bind₁	—	eval₂Hom_bind₁
aeval_bind₂ 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike aeval RingHom Semiring.toNonAssocSemiring RingHom.instFunLike bind₂ eval₂Hom RingHom.comp RingHomClass.toRingHom AlgHomClass.toRingHomClass AlgHom.algHomClass	—	eval₂Hom_bind₂
aeval_comp_bind₁ 📖	mathematical	—	AlgHom.comp MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id aeval bind₁ DFunLike.coe AlgHom AlgHom.funLike	—	algHom_ext aeval_bind₁
aeval_eq_bind₁ 📖	mathematical	—	aeval MvPolynomial commSemiring algebra Algebra.id bind₁	—	—
aeval_id_eq_join₁ 📖	mathematical	—	aeval MvPolynomial commSemiring algebra Algebra.id join₁	—	—
aeval_id_rename 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike aeval rename	—	aeval_rename
bind₁_C_right 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike bind₁ RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C	—	algHom_C
bind₁_X_left 📖	mathematical	—	bind₁ X AlgHom.id MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id	—	algHom_ext bind₁_X_right
bind₁_X_right 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike bind₁ X	—	aeval_X
bind₁_bind₁ 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike bind₁	—	—
bind₁_comp_bind₁ 📖	mathematical	—	AlgHom.comp MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id bind₁ DFunLike.coe AlgHom AlgHom.funLike	—	algHom_ext bind₁_bind₁
bind₁_comp_rename 📖	mathematical	—	AlgHom.comp MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id bind₁ rename	—	algHom_ext rename_X bind₁_X_right
bind₁_id 📖	mathematical	—	bind₁ MvPolynomial join₁	—	—
bind₁_monomial 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike bind₁ LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule module LinearMap.instFunLike monomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib RingHom RingHom.instFunLike C Finset.prod CommSemiring.toCommMonoid Finsupp.support MulZeroClass.toZero Nat.instMulZeroClass Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Finsupp Finsupp.instFunLike	—	monomial_eq Finset.prod_congr map_mul NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass bind₁_C_right map_prod MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass map_pow bind₁_X_right
bind₁_rename 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike bind₁ rename	—	AlgHom.congr_fun bind₁_comp_rename
bind₂_C_left 📖	mathematical	—	bind₂ C RingHom.id MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring	—	ringHom_ext' RingHom.ext bind₂_C_right RingHomCompTriple.comp_eq RingHomCompTriple.right_ids ext bind₂_X_right
bind₂_C_right 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike bind₂ C	—	eval₂Hom_C
bind₂_X_right 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike bind₂ X	—	eval₂Hom_X'
bind₂_bind₂ 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike bind₂ RingHom.comp	—	RingHom.congr_fun bind₂_comp_bind₂
bind₂_comp_C 📖	mathematical	—	RingHom.comp MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring bind₂ C	—	RingHom.ext bind₂_C_right
bind₂_comp_bind₂ 📖	mathematical	—	RingHom.comp MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring bind₂	—	ringHom_ext' RingHom.ext bind₂_C_right bind₂_comp_C ext bind₂_X_right
bind₂_id 📖	mathematical	—	bind₂ MvPolynomial commSemiring RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring join₂	—	—
bind₂_map 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike bind₂ map RingHom.comp	—	eval₂Hom_map_hom
bind₂_monomial 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike bind₂ LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule module LinearMap.instFunLike monomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	monomial_eq Finset.prod_congr map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass bind₂_C_right map_prod MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass map_pow bind₂_X_right one_mul
bind₂_monomial_one 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike bind₂ LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule module LinearMap.instFunLike monomial AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	bind₂_monomial RingHom.map_one one_mul
eval₂Hom_C_eq_bind₁ 📖	mathematical	—	eval₂Hom MvPolynomial commSemiring C RingHomClass.toRingHom AlgHom CommSemiring.toSemiring algebra Algebra.id AlgHom.funLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass AlgHom.algHomClass bind₁	—	—
eval₂Hom_C_id_eq_join₁ 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike eval₂Hom C AlgHom algebra Algebra.id AlgHom.funLike join₁	—	—
eval₂Hom_C_left 📖	mathematical	—	eval₂Hom MvPolynomial commSemiring C RingHomClass.toRingHom AlgHom CommSemiring.toSemiring algebra Algebra.id AlgHom.funLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass AlgHom.algHomClass bind₁	—	eval₂Hom_C_eq_bind₁
eval₂Hom_bind₁ 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike eval₂Hom AlgHom algebra Algebra.id AlgHom.funLike bind₁	—	hom_bind₁ eval₂Hom_comp_C
eval₂Hom_bind₂ 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike eval₂Hom bind₂ RingHom.comp	—	RingHom.congr_fun eval₂Hom_comp_bind₂
eval₂Hom_comp_C 📖	mathematical	—	RingHom.comp MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring eval₂Hom C	—	RingHom.ext eval₂_C
eval₂Hom_comp_bind₂ 📖	mathematical	—	RingHom.comp MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring eval₂Hom bind₂	—	ringHom_ext' RingHom.ext bind₂_C_right eval₂Hom_comp_C bind₂_X_right eval₂_X eval₂Hom_X'
eval₂Hom_eq_bind₂ 📖	mathematical	—	eval₂Hom MvPolynomial commSemiring X bind₂	—	—
eval₂Hom_id_X_eq_join₂ 📖	mathematical	—	eval₂Hom MvPolynomial commSemiring RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring X join₂	—	—
hom_bind₁ 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike AlgHom algebra Algebra.id AlgHom.funLike bind₁ eval₂Hom RingHom.comp C	—	bind₁.eq_1 map_aeval algebraMap_eq
join₁_rename 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike join₁ rename bind₁	—	aeval_id_rename
join₂_comp_map 📖	mathematical	—	RingHom.comp MvPolynomial commSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring join₂ map bind₂	—	RingHom.ext join₂_map
join₂_map 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial commSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike join₂ map bind₂	—	eval₂Hom_map_hom RingHom.id_comp
lawfulFunctor 📖	mathematical	—	MvPolynomial monad	—	rename_id rename_rename
lawfulMonad 📖	mathematical	—	MvPolynomial monad	—	lawfulFunctor bind₁_rename rename_id bind₁_X_right
map_bind₁ 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike map AlgHom algebra Algebra.id AlgHom.funLike bind₁	—	hom_bind₁ map_comp_C eval₂Hom_map_hom
map_bind₂ 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike map bind₂ RingHom.comp	—	eval₂_comp_right eval₂_map map_X
map_comp_C 📖	mathematical	—	RingHom.comp MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring map C	—	RingHom.ext map_C
mem_vars_bind₁ 📖	—	Finset Finset.instMembership vars DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike bind₁	—	—	vars_bind₁
rename_bind₁ 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike rename bind₁	—	AlgHom.congr_fun rename_comp_bind₁
rename_comp_bind₁ 📖	mathematical	—	AlgHom.comp MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id rename bind₁ DFunLike.coe AlgHom AlgHom.funLike	—	algHom_ext bind₁_X_right
vars_bind₁ 📖	mathematical	—	Finset Finset.instHasSubset vars DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike bind₁ Finset.biUnion	—	map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass as_sum vars_sum_subset bind₁_monomial Finset.biUnion_mono vars_mul vars_C Finset.empty_union vars_prod vars_pow mem_vars

---

← Back to Index