mul_induction_on — Mathlib

English

Theorem mul_induction_on: For C : R → Prop, r ∈ M * N, and hm, ha as in smul_induction_on with multiplication, C r holds.

Русский

Теорема mul_induction_on: для C : R → Prop, r ∈ M * N и аналогичных условий, C r выполняется.

LaTeX

$$$\text{MulInductionOn}(C, r, hm, ha): r \in M * N \Rightarrow (\forall m\in M, \forall n\in N, C(m n)) \to (\forall x,y, C(x) \to C(y) \to C(x+y)) \to C(r)$$$

Lean4

@[elab_as_elim]
protected theorem mul_induction_on {C : R → Prop} {r : R} (hr : r ∈ M * N) (hm : ∀ m ∈ M, ∀ n ∈ N, C (m * n))
    (ha : ∀ x y, C x → C y → C (x + y)) : C r :=
  AddSubmonoid.smul_induction_on hr hm ha

Похожие утверждения