Theorems · Theorem · order theory

ArchimedeanClass.mk_smul

∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {K : Type u_2}
  [inst_3 : Ring K] [inst_4 : LinearOrder K] [IsOrderedRing K] [Archimedean K] [inst_7 : Module K M] [PosSMulMono K M]
  (a : M) {k : K}, k ≠ 0 → ArchimedeanClass.mk (k • a) = ArchimedeanClass.mk a

Defined in

Mathlib.Algebra.Order.Module.Archimedean

Cited by

2 results in Mathlib

Foundations

Depth 31 from the axioms · uses propext, Quot.sound

Assumes

AddCommGroupLinearOrderIsOrderedAddMonoidRingLinearOrderIsOrderedRingArchimedeanModulePosSMulMono