Documentation

Groebner.AddEquiv

source
def AddEquiv.withBotCongr {α : Type u_1} {β : Type u_2} [Add α] [Add β] (e : α ≃+ β) :
WithBot α ≃+ WithBot β
Equations
Instances For
    source
    def AddEquiv.withTopCongr {α : Type u_1} {β : Type u_2} [Add α] [Add β] (e : α ≃+ β) :
    WithTop α ≃+ WithTop β
    Equations
    Instances For
      source
      @[simp]
      theorem AddEquiv.withBotCongr_toEquiv_eq {α : Type u_1} {β : Type u_2} [Add α] [Add β] (e : α ≃+ β) :
      e.withBotCongr.toEquiv = e.withBotCongr
      source
      @[simp]
      theorem AddEquiv.withTopCongr_toEquiv_eq {α : Type u_1} {β : Type u_2} [Add α] [Add β] (e : α ≃+ β) :
      e.withTopCongr.toEquiv = e.withTopCongr
      source
      @[simp]
      theorem AddEquiv.withBotCongr_toAddHom_eq {α : Type u_1} {β : Type u_2} [Add α] [Add β] (e : α ≃+ β) :
      e.withBotCongr.toAddHom = e.toAddHom.withBotMap
      source
      @[simp]
      theorem AddEquiv.withTopCongr_toAddHom_eq {α : Type u_1} {β : Type u_2} [Add α] [Add β] (e : α ≃+ β) :
      e.withTopCongr.toAddHom = e.toAddHom.withBotMap
      source
      @[simp]
      theorem AddEquiv.withBotCongr_apply {α : Type u_1} {β : Type u_2} [Add α] [Add β] (e : α ≃+ β) (a : WithBot α) :
      e.withBotCongr a = WithBot.map (⇑e) a
      source
      @[simp]
      theorem AddEquiv.withTopCongr_apply {α : Type u_1} {β : Type u_2} [Add α] [Add β] (e : α ≃+ β) (a : WithTop α) :
      e.withTopCongr a = WithTop.map (⇑e) a
      source
      @[simp]
      theorem AddEquiv.withBotCongr_refl {α : Type u_1} [Add α] :
      (refl α).withBotCongr = refl (WithBot α)
      source
      @[simp]
      theorem AddEquiv.withTopCongr_refl {α : Type u_1} [Add α] :
      (refl α).withTopCongr = refl (WithTop α)
      source
      @[simp]
      theorem AddEquiv.withBotCongr_symm {α : Type u_1} {β : Type u_2} [Add α] [Add β] (e : α ≃+ β) :
      e.symm.withBotCongr = e.withBotCongr.symm
      source
      @[simp]
      theorem AddEquiv.withTopCongr_symm {α : Type u_1} {β : Type u_2} [Add α] [Add β] (e : α ≃+ β) :
      e.symm.withTopCongr = e.withTopCongr.symm
      source
      @[simp]
      theorem AddEquiv.withBotCongr_trans {α : Type u_1} {β : Type u_3} {γ : Type u_2} [Add α] [Add β] [Add γ] (e₁ : α ≃+ β) (e₂ : β ≃+ γ) :
      (e₁.trans e₂).withBotCongr = e₁.withBotCongr.trans e₂.withBotCongr
      source
      @[simp]
      theorem AddEquiv.withTopCongr_trans {α : Type u_1} {β : Type u_3} {γ : Type u_2} [Add α] [Add β] [Add γ] (e₁ : α ≃+ β) (e₂ : β ≃+ γ) :
      (e₁.trans e₂).withTopCongr = e₁.withTopCongr.trans e₂.withTopCongr