Theorems · Theorem · order theory

Set.Ici_mul_Ici_eq

∀ {α : Type u_2} [inst : Monoid α] [inst_1 : Preorder α] [CanonicallyOrderedMul α] [MulRightMono α] {a b : α},
  Set.Ici a * Set.Ici b = Set.Ici (a * b)

Defined in: Mathlib.Algebra.Order.Group.Pointwise.Interval
Cited by: 0 results in Mathlib
Foundations: Depth 8 from the axioms · uses propext, Quot.sound
Assumes: Monoid Preorder CanonicallyOrderedMul MulRightMono

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites13

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement · cited by 53,352
Preorderstatement and proof · cited by 7,952
Monoidstatement and proof · cited by 3,887
Set.Icistatement and proof · cited by 1,070
Set.mulstatement · cited by 297
MulRightMonostatement and proof · cited by 263
Set.Subset.antisymmproof · cited by 213
CanonicallyOrderedMulstatement and proof · cited by 51
Set.mem_Iciproof · cited by 37
Set.subset_defproof · cited by 13
Set.mem_mulproof · cited by 12
ExistsMulOfLE.exists_mul_of_leproof · cited by 7

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.