English
There is an induction principle for IsBaseChange objects allowing to prove statements by building from zero, tmul, and addition under the base-change structure.
Русский
Существaет принцип индукции для объектов IsBaseChange, позволяющий доказывать утверждения, начиная с нуля, tmul и сложения внутри структуры базового изменения.
LaTeX
$$$\text{inductionOn}(x, \text{motive}, 0, \; \cdot, \; +) : \text{motive}(x)$$$
Lean4
@[elab_as_elim]
nonrec theorem inductionOn (x : N) (motive : N → Prop) (zero : motive 0) (tmul : ∀ m : M, motive (f m))
(smul : ∀ (s : S) (n), motive n → motive (s • n)) (add : ∀ n₁ n₂, motive n₁ → motive n₂ → motive (n₁ + n₂)) :
motive x :=
h.inductionOn x zero (fun _ _ => smul _ _ (tmul _)) add
