Documentation

Mathlib.Algebra.Group.WithOne.Basic

More operations on WithOne and WithZero #

This file defines various bundled morphisms on WithOne and WithZero that were not available in Algebra/Group/WithOne/Defs.

Main definitions #

theorem WithZero.involutiveNeg.proof_1 {α : Type u_1} [InvolutiveNeg α] (a : WithZero α) :
Option.map Neg.neg (Option.map Neg.neg a) = a
def WithZero.coeAddHom {α : Type u} [Add α] :

WithZero.coe as a bundled morphism

Instances For
    theorem WithZero.coeAddHom.proof_1 {α : Type u_1} [Add α] :
    ∀ (x x_1 : α), ↑(x + x_1) = ↑(x + x_1)
    @[simp]
    theorem WithOne.coeMulHom_apply {α : Type u} [Mul α] :
    ∀ (a : α), WithOne.coeMulHom a = a
    @[simp]
    theorem WithZero.coeAddHom_apply {α : Type u} [Add α] :
    ∀ (a : α), WithZero.coeAddHom a = a
    def WithOne.coeMulHom {α : Type u} [Mul α] :

    WithOne.coe as a bundled morphism

    Instances For
      def WithZero.lift {α : Type u} {β : Type v} [Add α] [AddZeroClass β] :
      AddHom α β (WithZero α →+ β)

      Lift an add semigroup homomorphism f to a bundled add monoid homorphism.

      Instances For
        theorem WithZero.lift.proof_2 {α : Type u_1} {β : Type u_2} [Add α] [AddZeroClass β] (f : AddHom α β) (x : WithZero α) (y : WithZero α) :
        ZeroHom.toFun { toFun := fun x => Option.casesOn x 0 f, map_zero' := (_ : (fun x => Option.casesOn x 0 f) 0 = (fun x => Option.casesOn x 0 f) 0) } (x + y) = ZeroHom.toFun { toFun := fun x => Option.casesOn x 0 f, map_zero' := (_ : (fun x => Option.casesOn x 0 f) 0 = (fun x => Option.casesOn x 0 f) 0) } x + ZeroHom.toFun { toFun := fun x => Option.casesOn x 0 f, map_zero' := (_ : (fun x => Option.casesOn x 0 f) 0 = (fun x => Option.casesOn x 0 f) 0) } y
        theorem WithZero.lift.proof_3 {α : Type u_2} {β : Type u_1} [Add α] [AddZeroClass β] (f : AddHom α β) :
        (fun F => AddHom.comp (F) WithZero.coeAddHom) ((fun f => { toZeroHom := { toFun := fun x => Option.casesOn x 0 f, map_zero' := (_ : (fun x => Option.casesOn x 0 f) 0 = (fun x => Option.casesOn x 0 f) 0) }, map_add' := (_ : ∀ (x y : WithZero α), ZeroHom.toFun { toFun := fun x => Option.casesOn x 0 f, map_zero' := (_ : (fun x => Option.casesOn x 0 f) 0 = (fun x => Option.casesOn x 0 f) 0) } (x + y) = ZeroHom.toFun { toFun := fun x => Option.casesOn x 0 f, map_zero' := (_ : (fun x => Option.casesOn x 0 f) 0 = (fun x => Option.casesOn x 0 f) 0) } x + ZeroHom.toFun { toFun := fun x => Option.casesOn x 0 f, map_zero' := (_ : (fun x => Option.casesOn x 0 f) 0 = (fun x => Option.casesOn x 0 f) 0) } y) }) f) = f
        theorem WithZero.lift.proof_1 {α : Type u_2} {β : Type u_1} [Add α] [AddZeroClass β] (f : AddHom α β) :
        (fun x => Option.casesOn x 0 f) 0 = (fun x => Option.casesOn x 0 f) 0
        theorem WithZero.lift.proof_4 {α : Type u_2} {β : Type u_1} [Add α] [AddZeroClass β] (F : WithZero α →+ β) :
        (fun f => { toZeroHom := { toFun := fun x => Option.casesOn x 0 f, map_zero' := (_ : (fun x => Option.casesOn x 0 f) 0 = (fun x => Option.casesOn x 0 f) 0) }, map_add' := (_ : ∀ (x y : WithZero α), ZeroHom.toFun { toFun := fun x => Option.casesOn x 0 f, map_zero' := (_ : (fun x => Option.casesOn x 0 f) 0 = (fun x => Option.casesOn x 0 f) 0) } (x + y) = ZeroHom.toFun { toFun := fun x => Option.casesOn x 0 f, map_zero' := (_ : (fun x => Option.casesOn x 0 f) 0 = (fun x => Option.casesOn x 0 f) 0) } x + ZeroHom.toFun { toFun := fun x => Option.casesOn x 0 f, map_zero' := (_ : (fun x => Option.casesOn x 0 f) 0 = (fun x => Option.casesOn x 0 f) 0) } y) }) ((fun F => AddHom.comp (F) WithZero.coeAddHom) F) = F
        def WithOne.lift {α : Type u} {β : Type v} [Mul α] [MulOneClass β] :
        (α →ₙ* β) (WithOne α →* β)

        Lift a semigroup homomorphism f to a bundled monoid homorphism.

        Instances For
          @[simp]
          theorem WithZero.lift_coe {α : Type u} {β : Type v} [Add α] [AddZeroClass β] (f : AddHom α β) (x : α) :
          ↑(WithZero.lift f) x = f x
          @[simp]
          theorem WithOne.lift_coe {α : Type u} {β : Type v} [Mul α] [MulOneClass β] (f : α →ₙ* β) (x : α) :
          ↑(WithOne.lift f) x = f x
          theorem WithZero.lift_zero {α : Type u} {β : Type v} [Add α] [AddZeroClass β] (f : AddHom α β) :
          ↑(WithZero.lift f) 0 = 0
          theorem WithOne.lift_one {α : Type u} {β : Type v} [Mul α] [MulOneClass β] (f : α →ₙ* β) :
          ↑(WithOne.lift f) 1 = 1
          theorem WithZero.lift_unique {α : Type u} {β : Type v} [Add α] [AddZeroClass β] (f : WithZero α →+ β) :
          f = WithZero.lift (AddHom.comp (f) WithZero.coeAddHom)
          theorem WithOne.lift_unique {α : Type u} {β : Type v} [Mul α] [MulOneClass β] (f : WithOne α →* β) :
          f = WithOne.lift (MulHom.comp (f) WithOne.coeMulHom)
          def WithZero.map {α : Type u} {β : Type v} [Add α] [Add β] (f : AddHom α β) :

          Given an additive map from α → β returns an add monoid homomorphism from WithZero α to WithZero β

          Instances For
            def WithOne.map {α : Type u} {β : Type v} [Mul α] [Mul β] (f : α →ₙ* β) :

            Given a multiplicative map from α → β returns a monoid homomorphism from WithOne α to WithOne β

            Instances For
              @[simp]
              theorem WithZero.map_coe {α : Type u} {β : Type v} [Add α] [Add β] (f : AddHom α β) (a : α) :
              ↑(WithZero.map f) a = ↑(f a)
              @[simp]
              theorem WithOne.map_coe {α : Type u} {β : Type v} [Mul α] [Mul β] (f : α →ₙ* β) (a : α) :
              ↑(WithOne.map f) a = ↑(f a)
              @[simp]
              theorem WithZero.map_map {α : Type u} {β : Type v} {γ : Type w} [Add α] [Add β] [Add γ] (f : AddHom α β) (g : AddHom β γ) (x : WithZero α) :
              ↑(WithZero.map g) (↑(WithZero.map f) x) = ↑(WithZero.map (AddHom.comp g f)) x
              theorem WithOne.map_map {α : Type u} {β : Type v} {γ : Type w} [Mul α] [Mul β] [Mul γ] (f : α →ₙ* β) (g : β →ₙ* γ) (x : WithOne α) :
              ↑(WithOne.map g) (↑(WithOne.map f) x) = ↑(WithOne.map (MulHom.comp g f)) x
              @[simp]
              theorem WithZero.map_comp {α : Type u} {β : Type v} {γ : Type w} [Add α] [Add β] [Add γ] (f : AddHom α β) (g : AddHom β γ) :
              @[simp]
              theorem WithOne.map_comp {α : Type u} {β : Type v} {γ : Type w} [Mul α] [Mul β] [Mul γ] (f : α →ₙ* β) (g : β →ₙ* γ) :
              theorem AddEquiv.withZeroCongr.proof_2 {α : Type u_2} {β : Type u_1} [Add α] [Add β] (e : α ≃+ β) :
              def AddEquiv.withZeroCongr {α : Type u} {β : Type v} [Add α] [Add β] (e : α ≃+ β) :

              A version of Equiv.optionCongr for WithZero.

              Instances For
                theorem AddEquiv.withZeroCongr.proof_3 {α : Type u_1} {β : Type u_2} [Add α] [Add β] (e : α ≃+ β) (x : WithZero α) (y : WithZero α) :
                theorem AddEquiv.withZeroCongr.proof_1 {α : Type u_1} {β : Type u_2} [Add α] [Add β] (e : α ≃+ β) :
                @[simp]
                theorem AddEquiv.withZeroCongr_apply {α : Type u} {β : Type v} [Add α] [Add β] (e : α ≃+ β) (a : WithZero α) :
                @[simp]
                theorem MulEquiv.withOneCongr_apply {α : Type u} {β : Type v} [Mul α] [Mul β] (e : α ≃* β) (a : WithOne α) :
                def MulEquiv.withOneCongr {α : Type u} {β : Type v} [Mul α] [Mul β] (e : α ≃* β) :

                A version of Equiv.optionCongr for WithOne.

                Instances For
                  @[simp]
                  theorem AddEquiv.withZeroCongr_trans {α : Type u} {β : Type v} {γ : Type w} [Add α] [Add β] [Add γ] (e₁ : α ≃+ β) (e₂ : β ≃+ γ) :
                  @[simp]
                  theorem MulEquiv.withOneCongr_trans {α : Type u} {β : Type v} {γ : Type w} [Mul α] [Mul β] [Mul γ] (e₁ : α ≃* β) (e₂ : β ≃* γ) :