mathlib3 documentation

algebra.order.monoid.to_mul_bot

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Making an additive monoid multiplicative then adding a zero is the same as adding a bottom element then making it multiplicative.

source
def with_zero.to_mul_bot {α : Type u} [has_add α] :
with_zero (multiplicative α) ≃* multiplicative (with_bot α)

Making an additive monoid multiplicative then adding a zero is the same as adding a bottom element then making it multiplicative.

Equations
source
@[simp]
theorem with_zero.to_mul_bot_zero {α : Type u} [has_add α] :
⇑with_zero.to_mul_bot 0 = ⇑multiplicative.of_add ⊥
source
@[simp]
theorem with_zero.to_mul_bot_coe {α : Type u} [has_add α] (x : multiplicative α) :
⇑with_zero.to_mul_bot ↑x = ⇑multiplicative.of_add ↑(⇑multiplicative.to_add x)
source
@[simp]
theorem with_zero.to_mul_bot_symm_bot {α : Type u} [has_add α] :
⇑(with_zero.to_mul_bot.symm) (⇑multiplicative.of_add ⊥) = 0
source
@[simp]
theorem with_zero.to_mul_bot_coe_of_add {α : Type u} [has_add α] (x : α) :
⇑(with_zero.to_mul_bot.symm) (⇑multiplicative.of_add ↑x) = ↑(⇑multiplicative.of_add x)
source
theorem with_zero.to_mul_bot_strict_mono {α : Type u} [has_add α] [preorder α] :
strict_mono ⇑with_zero.to_mul_bot
source
@[simp]
theorem with_zero.to_mul_bot_le {α : Type u} [has_add α] [preorder α] (a b : with_zero (multiplicative α)) :
⇑with_zero.to_mul_bot a ≤ ⇑with_zero.to_mul_bot b ↔ a ≤ b
source
@[simp]
theorem with_zero.to_mul_bot_lt {α : Type u} [has_add α] [preorder α] (a b : with_zero (multiplicative α)) :
⇑with_zero.to_mul_bot a < ⇑with_zero.to_mul_bot b ↔ a < b