mul_induction_on — Mathlib

English

Let C be a predicate on A. If C(m n) holds for all m ∈ M, n ∈ N, and C is closed under addition, then C holds for all r ∈ M * N.

Русский

Пусть C — свойство на A. Если C(m n) верно для всех m ∈ M, n ∈ N, и C сохраняется при сложении, то C верно для всех r ∈ M * N.

LaTeX

$$$ \forall r \in M * N, C(r) $ given the base and closure conditions$$

Lean4

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

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