English
Let M,N be submonoids and C a predicate on the ambient ring. If a ∈ M • N, and C is preserved by multiplying with elements of M and N, and C is closed under addition, then C holds for a.
Русский
Пусть M,N — подмножества-монойды и C — предикат на окружении. Если a ∈ M • N, и C сохраняется под умножением на элементы из M и N, и C замкну относительно сложения, то C выполняется для a.
LaTeX
$$$a \in M \cdot N \Rightarrow (\forall m \in M, \forall n \in N, C(m\cdot n)) \land (\forall x,y, C(x) \to C(y) \to C(x+y)) \Rightarrow C(a)$$$
Lean4
@[elab_as_elim]
protected theorem smul_induction_on {C : A → Prop} {a : A} (ha : a ∈ M • N) (hm : ∀ m ∈ M, ∀ n ∈ N, C (m • n))
(hadd : ∀ x y, C x → C y → C (x + y)) : C a :=
(@smul_le _ _ _ _ _ _ _ ⟨⟨setOf C, hadd _ _⟩, by simpa only [smul_zero] using hm _ (zero_mem _) _ (zero_mem _)⟩).2 hm
ha
