Documentation

Mathlib.Algebra.GroupWithZero.WithZero

Adjoining a zero to a group #

This file proves that one can adjoin a new zero element to a group and get a group with zero.

Main definitions #

instance WithZero.one {α : Type u_1} [One α] :
Equations
  • WithZero.one = let __spread.0 := inst; { one := One.one }
@[simp]
theorem WithZero.coe_one {α : Type u_1} [One α] :
1 = 1
instance WithZero.mulZeroClass {α : Type u_1} [Mul α] :
Equations
@[simp]
theorem WithZero.coe_mul {α : Type u_1} [Mul α] (a : α) (b : α) :
(a * b) = a * b
theorem WithZero.unzero_mul {α : Type u_1} [Mul α] {x : WithZero α} {y : WithZero α} (hxy : x * y 0) :
instance WithZero.noZeroDivisors {α : Type u_1} [Mul α] :
Equations
  • =
Equations
Equations
  • WithZero.commSemigroup = let __spread.0 := WithZero.semigroupWithZero; CommSemigroup.mk
Equations
@[simp]
theorem WithZero.coeMonoidHom_apply {α : Type u_1} [MulOneClass α] :
∀ (a : α), WithZero.coeMonoidHom a = a

Coercion as a monoid hom.

Equations
  • WithZero.coeMonoidHom = { toFun := WithZero.coe, map_one' := , map_mul' := }
Instances For
    theorem WithZero.monoidWithZeroHom_ext {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulZeroOneClass β] ⦃f : WithZero α →*₀ β ⦃g : WithZero α →*₀ β (h : (f).comp WithZero.coeMonoidHom = (g).comp WithZero.coeMonoidHom) :
    f = g
    @[simp]
    theorem WithZero.lift'_symm_apply_apply {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulZeroOneClass β] (F : WithZero α →*₀ β) :
    ∀ (a : α), (WithZero.lift'.symm F) a = F a
    noncomputable def WithZero.lift' {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulZeroOneClass β] :
    (α →* β) (WithZero α →*₀ β)

    The (multiplicative) universal property of WithZero.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem WithZero.lift'_zero {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulZeroOneClass β] (f : α →* β) :
      (WithZero.lift' f) 0 = 0
      @[simp]
      theorem WithZero.lift'_coe {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulZeroOneClass β] (f : α →* β) (x : α) :
      (WithZero.lift' f) x = f x
      theorem WithZero.lift'_unique {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulZeroOneClass β] (f : WithZero α →*₀ β) :
      f = WithZero.lift' ((f).comp WithZero.coeMonoidHom)
      noncomputable def WithZero.map' {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulOneClass β] (f : α →* β) :

      The MonoidWithZero homomorphism WithZero α →* WithZero β induced by a monoid homomorphism f : α →* β.

      Equations
      Instances For
        theorem WithZero.map'_zero {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulOneClass β] (f : α →* β) :
        @[simp]
        theorem WithZero.map'_coe {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulOneClass β] (f : α →* β) (x : α) :
        (WithZero.map' f) x = (f x)
        theorem WithZero.map'_map' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MulOneClass α] [MulOneClass β] [MulOneClass γ] (f : α →* β) (g : β →* γ) (x : WithZero α) :
        (WithZero.map' g) ((WithZero.map' f) x) = (WithZero.map' (g.comp f)) x
        @[simp]
        theorem WithZero.map'_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MulOneClass α] [MulOneClass β] [MulOneClass γ] (f : α →* β) (g : β →* γ) :
        WithZero.map' (g.comp f) = (WithZero.map' g).comp (WithZero.map' f)
        instance WithZero.pow {α : Type u_1} [One α] [Pow α ] :
        Equations
        • WithZero.pow = { pow := fun (x : WithZero α) (n : ) => match x, n with | none, 0 => 1 | none, n.succ => 0 | some x, n => (x ^ n) }
        @[simp]
        theorem WithZero.coe_pow {α : Type u_1} [One α] [Pow α ] (a : α) (n : ) :
        (a ^ n) = a ^ n
        Equations
        • WithZero.monoidWithZero = let __spread.0 := WithZero.mulZeroOneClass; let __spread.1 := WithZero.semigroupWithZero; MonoidWithZero.mk
        Equations
        • WithZero.commMonoidWithZero = let __src := WithZero.monoidWithZero; let __src_1 := WithZero.commSemigroup; CommMonoidWithZero.mk
        instance WithZero.inv {α : Type u_1} [Inv α] :

        Extend the inverse operation on α to WithZero α by sending 0 to 0.

        Equations
        @[simp]
        theorem WithZero.coe_inv {α : Type u_1} [Inv α] (a : α) :
        a⁻¹ = (a)⁻¹
        @[simp]
        theorem WithZero.inv_zero {α : Type u_1} [Inv α] :
        0⁻¹ = 0
        Equations
        instance WithZero.div {α : Type u_1} [Div α] :
        Equations
        theorem WithZero.coe_div {α : Type u_1} [Div α] (a : α) (b : α) :
        (a / b) = a / b
        instance WithZero.instPowInt {α : Type u_1} [One α] [Pow α ] :
        Equations
        • One or more equations did not get rendered due to their size.
        @[simp]
        theorem WithZero.coe_zpow {α : Type u_1} [One α] [Pow α ] (a : α) (n : ) :
        (a ^ n) = a ^ n
        Equations
        • WithZero.divInvMonoid = let __spread.0 := WithZero.monoidWithZero; DivInvMonoid.mk (fun (n : ) (a : WithZero α) => a ^ n)
        Equations
        • WithZero.divInvOneMonoid = let __spread.0 := WithZero.divInvMonoid; let __spread.1 := WithZero.invOneClass; DivInvOneMonoid.mk
        Equations
        Equations
        • WithZero.divisionMonoid = let __spread.0 := WithZero.divInvMonoid; let __spread.1 := WithZero.involutiveInv; DivisionMonoid.mk
        Equations
        • WithZero.divisionCommMonoid = let __spread.0 := WithZero.divisionMonoid; let __spread.1 := WithZero.commSemigroup; DivisionCommMonoid.mk
        instance WithZero.groupWithZero {α : Type u_1} [Group α] :

        If α is a group then WithZero α is a group with zero.

        Equations
        • WithZero.groupWithZero = let __spread.0 := WithZero.monoidWithZero; let __spread.1 := WithZero.divInvMonoid; let __spread.2 := ; GroupWithZero.mk DivInvMonoid.zpow

        Any group is isomorphic to the units of itself adjoined with 0.

        Equations
        • WithZero.unitsWithZeroEquiv = { toFun := fun (a : (WithZero α)ˣ) => WithZero.unzero , invFun := fun (a : α) => Units.mk0 a , left_inv := , right_inv := , map_mul' := }
        Instances For
          Equations
          • WithZero.commGroupWithZero = let __src := WithZero.groupWithZero; let __src_1 := WithZero.commMonoidWithZero; CommGroupWithZero.mk GroupWithZero.zpow
          Equations