WithZero.coe_mul
theorem WithZero.coe_mul : ∀ {α : Type u_1} [inst : Mul α] (a b : α), ↑(a * b) = ↑a * ↑b
This theorem states that for any type `α` equipped with a multiplication operation, the operation of lifting a multiplication result from this type to the type with zero (`WithZero α`) is equivalent to first lifting the individual elements to `WithZero α` and then multiplying them. In mathematical terms, for any elements `a` and `b` of type `α`, `↑(a * b) = ↑a * ↑b` where `↑` denotes the lifting operation, and `*` represents multiplication in either `α` or `WithZero α` depending on the context.
More concisely: For any type `α` with multiplication and a lifting operation to `WithZero α`, the lifted multiplication of elements equals the product of their lifted values: `↑(a * b) = ↑a * ↑b` for all `a, b` in `α`.
|
WithZero.coe_one
theorem WithZero.coe_one : ∀ {α : Type u_1} [inst : One α], ↑1 = 1
This theorem states that for any type `α` that has an instance of the `One` typeclass (meaning it has a designated "one" element), the "one" element of `α` when coerced into the `WithZero` type becomes the "one" element of the `WithZero` type. In other words, the "one" of any type is preserved when you map that type into the `WithZero` type.
More concisely: For any type `α` with a `One` instance, the coercion of its one element is equal to the one element of the `WithZero` type.
|