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 AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike map frobenius AlgHom AddMonoidAlgebra.semiring Finsupp.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike expand Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	map_frobenius_expand
map_expand_pow_char 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike map iterateFrobenius AlgHom AddMonoidAlgebra.semiring Finsupp.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike expand Monoid.toPow Nat.instMonoid MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	map_iterateFrobenius_expand
map_frobenius_expand 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike map frobenius AlgHom AddMonoidAlgebra.semiring Finsupp.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike expand Monoid.toPow 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 AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike map iterateFrobenius AlgHom AddMonoidAlgebra.semiring Finsupp.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike expand Monoid.toPow 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