Theorems · Theorem · ring theory

Unitization.ind

∀ {R : Type u_5} {A : Type u_6} [inst : AddZeroClass R] [inst_1 : AddZeroClass A] {P : Unitization R A → Prop},
  (∀ (r : R) (a : A), P (Unitization.inl r + ↑a)) → ∀ (x : Unitization R A), P x

To show a property hold on all Unitization R A it suffices to show it holds on terms of the form inl r + a. This can be used as induction x.

Defined in

Mathlib.Algebra.Algebra.Unitization

Cited by

6 results in Mathlib

Foundations

Depth 13 from the axioms · uses no axioms

Assumes

AddZeroClassAddZeroClass