Adjoining a zero to a group

This file contains basic inequality results on the unit subgroup of a group with an adjoined zero.

@[simp]

theorem WithZero.unitsWithZeroEquiv_units_val {α : Type u_1} [Group α] {γ : (WithZero α)ˣ} : ↑γ = ↑(WithZero.unitsWithZeroEquiv γ)

theorem WithZero.units_toAdd_le_of_le {α : Type u_2} [AddGroup α] [Preorder α] {γ : (WithZero (Multiplicative α))ˣ} {m : WithZero (Multiplicative α)} (hm : m ≠ 0) (hγ : ↑γ ≤ m) : Multiplicative.toAdd (WithZero.unitsWithZeroEquiv γ) ≤ Multiplicative.toAdd (WithZero.unzero hm)

theorem WithZero.units_toAdd_neg_add_of_le {α : Type u_2} [AddGroup α] [Preorder α] {γ : (WithZero (Multiplicative α))ˣ} [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] {m : WithZero (Multiplicative α)} (hm : m ≠ 0) (hγ : ↑γ ≤ m) : 0 ≤ -Multiplicative.toAdd (WithZero.unitsWithZeroEquiv γ) + Multiplicative.toAdd (WithZero.unzero hm)

theorem WithZero.units_toAdd_neg_add_one {α : Type u_2} [AddGroup α] [Preorder α] [One α] {γ : (WithZero (Multiplicative α))ˣ} [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [ZeroLEOneClass α] (hγ : ↑γ ≤ 1) : 0 ≤ -Multiplicative.toAdd (WithZero.unitsWithZeroEquiv γ) + 1