English
Let C be a property on ExteriorAlgebra R M. If C holds on all scalar images via algebraMap, on all ι_R(x) with x ∈ M, and is preserved under addition and multiplication, then C holds for every element of ExteriorAlgebra R M.
Русский
Пусть C — свойство на ExteriorAlgebra R M. Если C выполняется на всех образах скаляров через algebraMap, на всех ι_R(x) (x ∈ M), и сохраняется при сложении и умножении, то C выполняется для любого элемента ExteriorAlgebra R M.
LaTeX
$$$\text{induction} : (\forall r, C( algebraMap R (ExteriorAlgebra R M) r)) o (\forall x, C(ι R x)) o (\forall a b, C a \to C b \to C (a b)) o (\forall a b, C a \to C b \to C (a + b)) \to \forall a, C a$$$
Lean4
/-- If `C` holds for the `algebraMap` of `r : R` into `ExteriorAlgebra R M`, the `ι` of `x : M`,
and is preserved under addition and multiplication, then it holds for all of `ExteriorAlgebra R M`.
-/
@[elab_as_elim]
theorem induction {C : ExteriorAlgebra R M → Prop} (algebraMap : ∀ r, C (algebraMap R (ExteriorAlgebra R M) r))
(ι : ∀ x, C (ι R x)) (mul : ∀ a b, C a → C b → C (a * b)) (add : ∀ a b, C a → C b → C (a + b))
(a : ExteriorAlgebra R M) : C a :=
CliffordAlgebra.induction algebraMap ι mul add a
