Theorems · Theorem · group theory
Pi.mulSingle_induction
∀ {ι : Type u_1} [Finite ι] [inst : DecidableEq ι] {M : ι → Type u_7} [inst_1 : (i : ι) → CommMonoid (M i)]
(p : ((i : ι) → M i) → Prop) (f : (i : ι) → M i),
p 1 → (∀ (f g : (i : ι) → M i), p f → p g → p (f * g)) → (∀ (i : ι) (m : M i), p (Pi.mulSingle i m)) → p f- Defined in
- Mathlib.Algebra.BigOperators.Pi
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 73 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- FiniteDecidableEqCommMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Fintypeproof · cited by 7,736
- Finitestatement and proof · cited by 3,029
- CommMonoidstatement and proof · cited by 2,264
- nonempty_fintypeproof · cited by 261
- Pi.mulSinglestatement and proof · cited by 111
- Finset.prod_inductionproof · cited by 18
- Finset.univ_prod_mulSingleproof · cited by 2
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.