mul_induction_on — Mathlib

English

There is an inductive principle on products of fractional ideals: if a predicate holds for generators i ∈ I, j ∈ J, and is closed under sums, then it holds for all products i·j.

Русский

Существует индуктивный принцип по произведениям дробных идеалов: если тождество выполняется для порождающих и сохраняется суммами, оно выполняется для всех произведений.

LaTeX

$$$(hr) \Rightarrow (hm) (ha) \Rightarrow C(r)$$$

Lean4

@[elab_as_elim]
protected theorem mul_induction_on {I J : FractionalIdeal S P} {C : P → Prop} {r : P} (hr : r ∈ I * J)
    (hm : ∀ i ∈ I, ∀ j ∈ J, C (i * j)) (ha : ∀ x y, C x → C y → C (x + y)) : C r :=
  by
  simp only [mul_def] at hr
  exact Submodule.mul_induction_on hr hm ha

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