nonzero_of_invertible
theorem nonzero_of_invertible :
∀ {α : Type u} [inst : MulZeroOneClass α] (a : α) [inst_1 : Nontrivial α] [inst_2 : Invertible a], a ≠ 0
This theorem states that for any type `α` that has multiplication, zero, and one (i.e., it is a `MulZeroOneClass`), and for any element `a` of that type, if `a` is invertible and `α` is nontrivial (i.e., it contains at least two distinct elements), then `a` cannot be zero. This is a generalization from the field of mathematics where an invertible element in a ring or field is always non-zero.
More concisely: For any `MulZeroOneClass` type `α` with at least two elements, every invertible element `a` is non-zero.
|
invOf_eq_inv
theorem invOf_eq_inv : ∀ {α : Type u} [inst : GroupWithZero α] (a : α) [inst_1 : Invertible a], ⅟a = a⁻¹
This theorem states that for any type `α` that forms a group with a zero element (meaning it has operations for addition, multiplication, and a distinguished "zero" element, and these satisfy certain mathematical properties), if a given element `a` from this group is invertible (meaning that it has a multiplicative inverse), then its multiplicative inverse is equal to its inverse from the GroupWithZero structure. In other words, the notation `⅟a` (often used for the multiplicative inverse of `a`) is equivalent to `a⁻¹` (the notation for the inverse of `a` within a group structure).
More concisely: For any group with zero `α` and invertible element `a`, `⅟a = a⁻¹`.
|