FreeCommRing.induction_on
theorem FreeCommRing.induction_on :
∀ {α : Type u} {C : FreeCommRing α → Prop} (z : FreeCommRing α),
C (-1) →
(∀ (b : α), C (FreeCommRing.of b)) →
(∀ (x y : FreeCommRing α), C x → C y → C (x + y)) → (∀ (x y : FreeCommRing α), C x → C y → C (x * y)) → C z
The theorem `FreeCommRing.induction_on` in Lean 4 provides an induction principle for the free commutative ring on a type `α`. Given any type `α` and a property `C` that applies to elements of the free commutative ring on `α`, if `C` holds for the negative unity (-1), and if `C` is preserved under the canonical map from `α` to the free commutative ring on `α`, addition, and multiplication, then `C` holds for every element of the free commutative ring on `α`. This means that to prove a property for all elements of the free commutative ring, it is sufficient to prove it for the basic elements, and show that it is preserved under the ring operations.
More concisely: Given a property `C` on the free commutative ring on a type `α`, if `C` holds for the negative unity and is preserved under the ring operations, then `C` holds for every element of the free commutative ring on `α`.
|
FreeCommRing.lift_of
theorem FreeCommRing.lift_of :
∀ {α : Type u} {R : Type v} [inst : CommRing R] (f : α → R) (x : α),
(FreeCommRing.lift f) (FreeCommRing.of x) = f x
The theorem `FreeCommRing.lift_of` states that for any types `α` and `R`, where `R` has a commutative ring structure, and for any function `f` from `α` to `R`, and any element `x` of `α`, applying the lift of `f` to the result of `FreeCommRing.of` applied to `x` is equal to applying `f` directly to `x`. In other words, lifting `f` then applying it to the free commutative ring generated by `x` does not change the value of `f` at `x`. This theorem establishes the compatibility between the lift operation and the construction of an element in the free commutative ring.
More concisely: For any commutative ring `R`, function `f : α -> R`, and `x : α`, `FreeCommRing.lift_of R f x = f x`.
|