English
An induction principle: if a property holds for every mk a ha, then it holds for all FiniteMulArchimedeanClass M.
Русский
Индуктивный принцип: если свойство выполняется для каждого mk a ha, то оно верно и для всех FiniteMulArchimedeanClass M.
LaTeX
$$$\forall (motive : FiniteMulArchimedeanClass M \to Prop), (\forall a (ha : a \neq 1), motive (mk a ha)) \to \forall x, motive x$$$
Lean4
/-- An induction principle for `FiniteMulArchimedeanClass`. -/
@[to_additive (attr := elab_as_elim) /-- An induction principle for `FiniteArchimedeanClass`. -/
]
theorem ind {motive : FiniteMulArchimedeanClass M → Prop} (mk : ∀ a, (ha : a ≠ 1) → motive (.mk a ha)) :
∀ x, motive x := by simpa [FiniteMulArchimedeanClass, MulArchimedeanClass.forall]
