IsUnit.neg
theorem IsUnit.neg : ∀ {α : Type u} [inst : Monoid α] [inst_1 : HasDistribNeg α] {a : α}, IsUnit a → IsUnit (-a) := by
sorry
The theorem `IsUnit.neg` states that for any type `α` that is a monoid and has distributive negation, if an element `a` of `α` is a unit (i.e., it has a two-sided inverse), then the negation of `a` (denoted `-a`) is also a unit. In other words, the negation of a unit element in a monoid with distributive negation is also a unit element.
More concisely: If `α` is a monoid with distributive negation and `a` is a unit in `α`, then `-a` is also a unit.
|
IsUnit.neg_iff
theorem IsUnit.neg_iff : ∀ {α : Type u} [inst : Monoid α] [inst_1 : HasDistribNeg α] (a : α), IsUnit (-a) ↔ IsUnit a
The theorem `IsUnit.neg_iff` states that for any type `α`, that is a Monoid and also has a distributive negation, an element `a` of `α` is a unit if and only if its negation `-a` is a unit. In other words, in the context of a Monoid with distributive negation, an element and its negation are either both units or both non-units.
More concisely: In a Monoid equipped with distributive negation, an element and its negation are equal to the additive identity if and only if they are both units.
|
Units.val_neg
theorem Units.val_neg : ∀ {α : Type u} [inst : Monoid α] [inst_1 : HasDistribNeg α] (u : αˣ), ↑(-u) = -↑u
This theorem states that for any element `u` of the unit group of a ring `α`, representing `u` as an element of the ring, and then taking its negative, is the same as first taking the negative of `u` in the unit group, and then representing the result as an element of the ring. Here, `αˣ` refers to the unit group of the ring, i.e., the set of invertible elements under multiplication, and `-u` and `-↑u` denotes the additive inverses in the unit group and the ring, respectively.
More concisely: For any unit `u` in a ring `α`, the negative of `u` as an element of the ring is equivalent to the negative of the unit `u` in the multiplicative group of units.
|