Documentation

Mathlib.Algebra.GroupWithZero.Units.Lemmas

Further lemmas about units in a MonoidWithZero or a GroupWithZero. #

source
theorem IsUnit.map_ringInverse {M₀ : Type u_2} {M₀' : Type u_4} {F : Type u_6} [MonoidWithZero M₀] [MonoidWithZero M₀'] [FunLike F M₀ M₀'] [MonoidHomClass F M₀ M₀'] (f : F) {a : M₀} (h : IsUnit a) :
f (Ring.inverse a) = Ring.inverse (f a)
source
theorem map_ringInverse {M₀ : Type u_2} {M₀' : Type u_4} {F : Type u_6} [MonoidWithZero M₀] [MonoidWithZero M₀'] [FunLike F M₀ M₀'] [MonoidWithZeroHomClass F M₀ M₀'] (f : F) [IsLocalHom f] (a : M₀) :
f (Ring.inverse a) = Ring.inverse (f a)

A homomorphism which reflects units commutes with Ring.inverse. This does not require any IsUnit assumption. The IsLocalHom f hypothesis is satisfied when f is an isomorphism. Not marked simp to prevent frequent instance searches for IsLocalHom _.

source
theorem isLocalHom_iff_map_ringInverse {M₀ : Type u_2} {M₀' : Type u_4} {F : Type u_6} [MonoidWithZero M₀] [MonoidWithZero M₀'] [FunLike F M₀ M₀'] [MonoidWithZeroHomClass F M₀ M₀'] [Nontrivial M₀'] (f : F) :
IsLocalHom f ↔ ∀ (a : M₀), f (Ring.inverse a) = Ring.inverse (f a)
source
theorem isLocalHom_of_exists_map_ne_one {M : Type u_1} {G₀ : Type u_3} {F : Type u_6} [Monoid M] [GroupWithZero G₀] [FunLike F G₀ M] [MonoidHomClass F G₀ M] {f : F} (hf : ∃ (x : G₀), f x ≠ 1) :
IsLocalHom f
source
instance instIsLocalHomOfMonoidWithZeroHomClassOfNontrivial {M₀ : Type u_2} {G₀ : Type u_3} {F : Type u_6} [MonoidWithZero M₀] [GroupWithZero G₀] [FunLike F G₀ M₀] [MonoidWithZeroHomClass F G₀ M₀] [Nontrivial M₀] (f : F) :
IsLocalHom f
source
theorem map_inv_eq_ringInverse_map {M₀ : Type u_2} {G₀ : Type u_3} {F : Type u_6} [MonoidWithZero M₀] [GroupWithZero G₀] [FunLike F G₀ M₀] [MonoidWithZeroHomClass F G₀ M₀] (f : F) (a : G₀) :
f a⁻¹ = Ring.inverse (f a)
source
theorem Commute.div_eq_div_iff {G₀ : Type u_3} [GroupWithZero G₀] {a b c d : G₀} (hbd : Commute b d) (hb : b ≠ 0) (hd : d ≠ 0) :
a / b = c / d ↔ a * d = c * b

The MonoidWithZero version of div_eq_div_iff_mul_eq_mul.

source
theorem Commute.mul_inv_eq_mul_inv_iff {G₀ : Type u_3} [GroupWithZero G₀] {a b c d : G₀} (hbd : Commute b d) (hb : b ≠ 0) (hd : d ≠ 0) :
a * b⁻¹ = c * d⁻¹ ↔ a * d = c * b

The MonoidWithZero version of mul_inv_eq_mul_inv_iff_mul_eq_mul.

source
theorem Commute.inv_mul_eq_inv_mul_iff {G₀ : Type u_3} [GroupWithZero G₀] {a b c d : G₀} (hbd : Commute b d) (hb : b ≠ 0) (hd : d ≠ 0) :
b⁻¹ * a = d⁻¹ * c ↔ d * a = b * c

The MonoidWithZero version of inv_mul_eq_inv_mul_iff_mul_eq_mul.

source
theorem map_ne_zero {G₀ : Type u_3} {M₀' : Type u_4} {F : Type u_6} [GroupWithZero G₀] [MulZeroOneClass M₀'] [Nontrivial M₀'] [FunLike F G₀ M₀'] [MonoidWithZeroHomClass F G₀ M₀'] (f : F) {a : G₀} :
f a ≠ 0 ↔ a ≠ 0
source
@[simp]
theorem map_eq_zero {G₀ : Type u_3} {M₀' : Type u_4} {F : Type u_6} [GroupWithZero G₀] [MulZeroOneClass M₀'] [Nontrivial M₀'] [FunLike F G₀ M₀'] [MonoidWithZeroHomClass F G₀ M₀'] (f : F) {a : G₀} :
f a = 0 ↔ a = 0
source
theorem eq_on_inv₀ {G₀ : Type u_3} {M₀' : Type u_4} {F' : Type u_7} [GroupWithZero G₀] [MonoidWithZero M₀'] [FunLike F' G₀ M₀'] {a : G₀} [MonoidWithZeroHomClass F' G₀ M₀'] (f g : F') (h : f a = g a) :
f a⁻¹ = g a⁻¹
source
@[simp]
theorem map_inv₀ {G₀ : Type u_3} {G₀' : Type u_5} {F : Type u_6} [GroupWithZero G₀] [GroupWithZero G₀'] [FunLike F G₀ G₀'] [MonoidWithZeroHomClass F G₀ G₀'] (f : F) (a : G₀) :
f a⁻¹ = (f a)⁻¹

A monoid homomorphism between groups with zeros sending 0 to 0 sends a⁻¹ to (f a)⁻¹.

source
@[simp]
theorem map_div₀ {G₀ : Type u_3} {G₀' : Type u_5} {F : Type u_6} [GroupWithZero G₀] [GroupWithZero G₀'] [FunLike F G₀ G₀'] [MonoidWithZeroHomClass F G₀ G₀'] (f : F) (a b : G₀) :
f (a / b) = f a / f b
source
noncomputable def MonoidWithZero.inverse {M : Type u_8} [CommMonoidWithZero M] :
M →*₀ M

We define the inverse as a MonoidWithZeroHom by extending the inverse map by zero on non-units.

Equations
Instances For
    source
    @[simp]
    theorem MonoidWithZero.coe_inverse {M : Type u_8} [CommMonoidWithZero M] :
    ⇑inverse = Ring.inverse
    source
    @[simp]
    theorem MonoidWithZero.inverse_apply {M : Type u_8} [CommMonoidWithZero M] (a : M) :
    inverse a = Ring.inverse a
    source
    def invMonoidWithZeroHom {G₀ : Type u_8} [CommGroupWithZero G₀] :
    G₀ →*₀ G₀

    Inversion on a commutative group with zero, considered as a monoid with zero homomorphism.

    Equations
    Instances For
      source
      @[simp]
      theorem map_zpow₀ {F : Type u_8} {G₀ : Type u_9} {G₀' : Type u_10} [GroupWithZero G₀] [GroupWithZero G₀'] [FunLike F G₀ G₀'] [MonoidWithZeroHomClass F G₀ G₀'] (f : F) (x : G₀) (n : ℤ) :
      f (x ^ n) = f x ^ n

      If a monoid homomorphism f between two GroupWithZeros maps 0 to 0, then it maps x^n, n : ℤ, to (f x)^n.