Expand

📁 Source: Mathlib/RingTheory/MvPolynomial/Expand.lean

Statistics

Metric	Count
Definitions	0
Theorems expand_char, map_expand_pow_char, map_frobenius_expand, map_iterateFrobenius_expand	4
Total	4

MvPolynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
expand_char 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike map frobenius AlgHom algebra Algebra.id AlgHom.funLike expand Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	map_frobenius_expand
map_expand_pow_char 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike map iterateFrobenius AlgHom algebra Algebra.id AlgHom.funLike expand Monoid.toNatPow Nat.instMonoid MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	map_iterateFrobenius_expand
map_frobenius_expand 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike map frobenius AlgHom algebra Algebra.id AlgHom.funLike expand Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	induction_on' add_pow_expChar expand_monomial map_monomial monomial_pow map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass instExpChar
map_iterateFrobenius_expand 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike map iterateFrobenius AlgHom algebra Algebra.id AlgHom.funLike expand Monoid.toNatPow Nat.instMonoid MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	iterateFrobenius_zero pow_zero expand_one map_id pow_one pow_succ pow_mul map_frobenius_expand pow_succ' iterateFrobenius.congr_simp add_comm iterateFrobenius_add iterateFrobenius_one

---

← Back to Index