class ZeroNeTopClass (M : Type u_3) [Zero M] [Top M] : Prop

A class for the property that 0 ≠ ⊤.

• zero_ne_top : 0 ≠ ⊤

class OneNeTopClass (M : Type u_3) [One M] [Top M] : Prop

A class for the property that 1 ≠ ⊤.

• one_ne_top : 1 ≠ ⊤

@[simp]

theorem one_ne_top {M : Type u_1} [One M] [Top M] [OneNeTopClass M] : 1 ≠ ⊤

theorem zero_ne_top {M : Type u_1} [Zero M] [Top M] [ZeroNeTopClass M] : 0 ≠ ⊤

class AddEqTopClass (M : Type u_3) [Zero M] [Add M] [Top M] extends ZeroNeTopClass M : Prop

An AddEqTopClass is one where the top element is nonzero, and is not the sum of two non-top elements. Equivalently, the non-top elements are an additive submonoid.

• zero_ne_top : 0 ≠ ⊤
• eq_or_eq_of_add (a b : M) : a + b = ⊤ → a = ⊤ ∨ b = ⊤

class MulEqTopClass (M : Type u_3) [One M] [Mul M] [Top M] extends OneNeTopClass M : Prop

A MulEqTopClass is one where the top element is not 1, and is not the product of two non-top elements. Equivalently, the non-top elements are a submonoid.

• one_ne_top : 1 ≠ ⊤
• eq_or_eq_of_mul (a b : M) : a * b = ⊤ → a = ⊤ ∨ b = ⊤

theorem mul_ne_top {M : Type u_1} [One M] [Mul M] [Top M] [MulEqTopClass M] {a b : M} (ha : a ≠ ⊤) (hb : b ≠ ⊤) : a * b ≠ ⊤

theorem add_ne_top {M : Type u_1} [Zero M] [Add M] [Top M] [AddEqTopClass M] {a b : M} (ha : a ≠ ⊤) (hb : b ≠ ⊤) : a + b ≠ ⊤

theorem eq_or_eq_of_mul_eq_top {M : Type u_1} [One M] [Mul M] [Top M] [MulEqTopClass M] {a b : M} (h : a * b = ⊤) : a = ⊤ ∨ b = ⊤

theorem eq_or_eq_of_add_eq_top {M : Type u_1} [Zero M] [Add M] [Top M] [AddEqTopClass M] {a b : M} (h : a + b = ⊤) : a = ⊤ ∨ b = ⊤

theorem exists_of_prod_eq_top {M : Type u_1} {α : Type u_2} [CommMonoid M] [Top M] [MulEqTopClass M] {s : Finset α} {f : α → M} (h : ∏ x ∈ s, f x = ⊤) : ∃ (x : α), f x = ⊤

theorem exists_of_sum_eq_top {M : Type u_1} {α : Type u_2} [AddCommMonoid M] [Top M] [AddEqTopClass M] {s : Finset α} {f : α → M} (h : ∑ x ∈ s, f x = ⊤) : ∃ (x : α), f x = ⊤

def Submonoid.neTop (M : Type u_3) [Monoid M] [Top M] [MulEqTopClass M] : Submonoid M

The set of non-top elements in a MulEqTopClass is a submonoid.

Equations

• Submonoid.neTop M = { carrier := {x : M | x ≠ ⊤}, mul_mem' := ⋯, one_mem' := ⋯ }

def AddSubmonoid.neTop (M : Type u_3) [AddMonoid M] [Top M] [AddEqTopClass M] : AddSubmonoid M

Equations

• AddSubmonoid.neTop M = { carrier := {x : M | x ≠ ⊤}, add_mem' := ⋯, zero_mem' := ⋯ }

@[simp]

theorem Submonoid.coe_neTop (M : Type u_3) [Monoid M] [Top M] [MulEqTopClass M] : ↑(neTop M) = {x : M | x ≠ ⊤}

class AddTopClass (M : Type u_3) [Add M] [Top M] : Prop

A mixin class for the property that ⊤ is additively absorbing.

• add_top (a : M) : a + ⊤ = ⊤
• top_add (a : M) : ⊤ + a = ⊤

class MulTopClass (M : Type u_3) [Mul M] [Top M] : Prop

A mixin class for the property that ⊤ is multiplicatively absorbing.

• mul_top (a : M) : a * ⊤ = ⊤
• top_mul (a : M) : ⊤ * a = ⊤

class PosMulTopClass (M : Type u_3) [Zero M] [Top M] [Mul M] [LT M] : Prop

A mixin class for the property that ⊤ multiplicatively absorbs positive elements.

• mul_top_of_pos {a : M} (ha : 0 < a) : a * ⊤ = ⊤
• top_mul_of_pos {a : M} (ha : 0 < a) : ⊤ * a = ⊤

theorem mul_top_of_pos {M : Type u_3} [Zero M] [Top M] [Mul M] [LT M] [PosMulTopClass M] {a : M} (ha : 0 < a) : a * ⊤ = ⊤

theorem top_mul_of_pos {M : Type u_3} [Zero M] [Top M] [Mul M] [LT M] [PosMulTopClass M] {a : M} (ha : 0 < a) : ⊤ * a = ⊤

@[simp]

theorem mul_top' {M : Type u_1} [Mul M] [Top M] [MulTopClass M] (a : M) : a * ⊤ = ⊤

theorem add_top' {M : Type u_1} [Add M] [Top M] [AddTopClass M] (a : M) : a + ⊤ = ⊤

@[simp]

theorem top_mul' {M : Type u_1} [Mul M] [Top M] [MulTopClass M] (a : M) : ⊤ * a = ⊤

theorem top_add' {M : Type u_1} [Add M] [Top M] [AddTopClass M] (a : M) : ⊤ + a = ⊤

instance instPosMulTopClassOfMulTopClass {M : Type u_1} [Zero M] [Top M] [Mul M] [LT M] [MulTopClass M] : PosMulTopClass M

@[simp]

theorem mul_eq_top_iff {M : Type u_1} [One M] [Mul M] [Top M] [MulTopClass M] [MulEqTopClass M] {a b : M} : a * b = ⊤ ↔ a = ⊤ ∨ b = ⊤

theorem add_eq_top_iff {M : Type u_1} [Zero M] [Add M] [Top M] [AddTopClass M] [AddEqTopClass M] {a b : M} : a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤

def Subsemiring.neTop (α : Type u_3) [DecidableEq α] [Semiring α] [PartialOrder α] [CanonicallyOrderedAdd α] [NoZeroDivisors α] [OrderTop α] [MulEqTopClass α] [AddEqTopClass α] : Subsemiring α

The set of non-top elements in a ring with MulEqTopClass, AddEqTopClass is a subring.

Equations

• Subsemiring.neTop α = { carrier := {x : α | x ≠ ⊤}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯ }

@[simp]

theorem Subsemiring.coe_neTop (α : Type u_3) [DecidableEq α] [Semiring α] [PartialOrder α] [CanonicallyOrderedAdd α] [NoZeroDivisors α] [OrderTop α] [MulEqTopClass α] [AddEqTopClass α] : ↑(neTop α) = {x : α | x ≠ ⊤}

instance instAddTopClass {M : Type u_3} [LinearOrderedAddCommMonoidWithTop M] : AddTopClass M

instance instAddEqTopClassOfNontrivial {M : Type u_3} [LinearOrderedAddCommMonoidWithTop M] [Nontrivial M] : AddEqTopClass M

@[instance_reducible]

instance instCommMonoidWithZeroSubtypeMemSubmonoidNeTopOfZeroNeTopClass {M : Type u_3} [CommMonoidWithZero M] [Preorder M] [OrderTop M] [MulEqTopClass M] [ZeroNeTopClass M] : CommMonoidWithZero ↥(Submonoid.neTop M)

Equations

• instCommMonoidWithZeroSubtypeMemSubmonoidNeTopOfZeroNeTopClass = { toCommMonoid := (Submonoid.neTop M).toCommMonoid, zero := ⟨0, ⋯⟩, zero_mul := ⋯, mul_zero := ⋯ }

theorem isRegular_of_ne_top {M : Type u_3} [CommMonoid M] [PartialOrder M] [OrderTop M] [MulEqTopClass M] [MulTopClass M] {x : M} [IsCancelMul ↥(Submonoid.neTop M)] (hx : x ≠ ⊤) : IsRegular x

theorem isAddRegular_of_ne_top {M : Type u_3} [AddCommMonoid M] [PartialOrder M] [OrderTop M] [AddEqTopClass M] [AddTopClass M] {x : M} [IsCancelAdd ↥(AddSubmonoid.neTop M)] (hx : x ≠ ⊤) : IsAddRegular x

theorem mul_le_mul_iff_left_of_ne_top' {M : Type u_3} [CommMonoid M] [PartialOrder M] [OrderTop M] [MulEqTopClass M] [MulTopClass M] {x y z : M} [IsOrderedCancelMonoid ↥(Submonoid.neTop M)] (hx : x ≠ ⊤) : x * y ≤ x * z ↔ y ≤ z

theorem add_le_add_iff_left_of_ne_top' {M : Type u_3} [AddCommMonoid M] [PartialOrder M] [OrderTop M] [AddEqTopClass M] [AddTopClass M] {x y z : M} [IsOrderedCancelAddMonoid ↥(AddSubmonoid.neTop M)] (hx : x ≠ ⊤) : x + y ≤ x + z ↔ y ≤ z

theorem mul_le_mul_iff_right_of_ne_top' {M : Type u_3} [CommMonoid M] [PartialOrder M] [OrderTop M] [MulEqTopClass M] [MulTopClass M] {x y z : M} [IsOrderedCancelMonoid ↥(Submonoid.neTop M)] (hx : x ≠ ⊤) : y * x ≤ z * x ↔ y ≤ z

theorem add_le_add_iff_right_of_ne_top' {M : Type u_3} [AddCommMonoid M] [PartialOrder M] [OrderTop M] [AddEqTopClass M] [AddTopClass M] {x y z : M} [IsOrderedCancelAddMonoid ↥(AddSubmonoid.neTop M)] (hx : x ≠ ⊤) : y + x ≤ z + x ↔ y ≤ z

theorem mul_lt_mul_iff_right_of_ne_top' {M : Type u_3} [CommMonoid M] [PartialOrder M] [OrderTop M] [MulEqTopClass M] [MulTopClass M] {x y z : M} [IsOrderedCancelMonoid ↥(Submonoid.neTop M)] (hx : x ≠ ⊤) : y * x < z * x ↔ y < z

theorem add_lt_add_iff_right_of_ne_top' {M : Type u_3} [AddCommMonoid M] [PartialOrder M] [OrderTop M] [AddEqTopClass M] [AddTopClass M] {x y z : M} [IsOrderedCancelAddMonoid ↥(AddSubmonoid.neTop M)] (hx : x ≠ ⊤) : y + x < z + x ↔ y < z

theorem mul_lt_mul_iff_left_of_ne_top' {M : Type u_3} [CommMonoid M] [PartialOrder M] [OrderTop M] [MulEqTopClass M] [MulTopClass M] {x y z : M} [IsOrderedCancelMonoid ↥(Submonoid.neTop M)] (hx : x ≠ ⊤) : x * y < x * z ↔ y < z

theorem add_lt_add_iff_left_of_ne_top' {M : Type u_3} [AddCommMonoid M] [PartialOrder M] [OrderTop M] [AddEqTopClass M] [AddTopClass M] {x y z : M} [IsOrderedCancelAddMonoid ↥(AddSubmonoid.neTop M)] (hx : x ≠ ⊤) : x + y < x + z ↔ y < z

theorem mul_right_strictMono_of_pos_of_ne_top {M : Type u_4} [CommMonoidWithZero M] [PartialOrder M] [OrderTop M] [MulEqTopClass M] [ZeroNeTopClass M] [PosMulTopClass M] [PosMulStrictMono ↥(Submonoid.neTop M)] {a : M} (h₀ : 0 < a) (hinf : a ≠ ⊤) : StrictMono fun (x : M) => a * x

theorem mul_left_strictMono_of_pos_of_ne_top {M : Type u_4} [CommMonoidWithZero M] [PartialOrder M] [OrderTop M] [MulEqTopClass M] [ZeroNeTopClass M] [PosMulTopClass M] [PosMulStrictMono ↥(Submonoid.neTop M)] {a : M} (h₀ : 0 < a) (hinf : a ≠ ⊤) : StrictMono fun (x : M) => x * a

@[simp]

theorem mul_lt_mul_iff_left₀_of_ne_top {M : Type u_4} [CommMonoidWithZero M] [LinearOrder M] [OrderTop M] [MulEqTopClass M] [ZeroNeTopClass M] [PosMulTopClass M] [PosMulStrictMono ↥(Submonoid.neTop M)] {a b c : M} (a0 : 0 < a) (ha : a ≠ ⊤) : b * a < c * a ↔ b < c

@[simp]

theorem mul_lt_mul_iff_right₀_of_ne_top {M : Type u_4} [CommMonoidWithZero M] [LinearOrder M] [OrderTop M] [MulEqTopClass M] [ZeroNeTopClass M] [PosMulTopClass M] [PosMulStrictMono ↥(Submonoid.neTop M)] {a b c : M} (a0 : 0 < a) (ha : a ≠ ⊤) : a * b < a * c ↔ b < c

instance instMulEqTopClassWithTopOfPreorder {M : Type u_1} [DecidableEq M] [CommMonoidWithZero M] [Preorder M] : MulEqTopClass (WithTop M)

instance instAddEqTopClassWithTopOfPreorder {M : Type u_1} [AddCommMonoid M] [Preorder M] : AddEqTopClass (WithTop M)

instance instNontrivialOfMulEqTopClass {M : Type u_1} [Mul M] [Top M] [One M] [MulEqTopClass M] : Nontrivial M

def orderAddMonoidIsoNeTop (M : Type u_3) [AddCommMonoid M] [Preorder M] : ↥(AddSubmonoid.neTop (WithTop M)) ≃+o M

The submonoid of non-top elements in WithTop M is isomorphic to M.

Equations

• One or more equations did not get rendered due to their size.

instance instIsCancelAddSubtypeWithTopMemAddSubmonoidNeTop {M : Type u_1} [AddCommMonoid M] [IsCancelAdd M] [Preorder M] : IsCancelAdd ↥(AddSubmonoid.neTop (WithTop M))

instance instIsOrderedCancelAddMonoidSubtypeWithTopMemAddSubmonoidNeTop {M : Type u_1} [AddCommMonoid M] [Preorder M] [IsOrderedCancelAddMonoid M] : IsOrderedCancelAddMonoid ↥(AddSubmonoid.neTop (WithTop M))

instance instMulEqTopClassWithTop {R : Type u_3} [DecidableEq R] [Semiring R] [PartialOrder R] [CanonicallyOrderedAdd R] [NoZeroDivisors R] [Nontrivial R] : MulEqTopClass (WithTop R)

def orderRingIsoNeTop (R : Type u_4) [DecidableEq R] [Semiring R] [PartialOrder R] [CanonicallyOrderedAdd R] [NoZeroDivisors R] [Nontrivial R] : ↥(Subsemiring.neTop (WithTop R)) ≃+*o R

The subring of non-top elements in WithTop R is isomorphic to R.

Equations

• One or more equations did not get rendered due to their size.