Theorems · Theorem · order theory

FiniteMulArchimedeanClass.coe_congrOrderIso_apply

∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {N : Type u_2}
  [inst_3 : CommGroup N] [inst_4 : LinearOrder N] [inst_5 : IsOrderedMonoid N]
  (e : MulArchimedeanClass M ≃o MulArchimedeanClass N) (a : FiniteMulArchimedeanClass M),
  ↑((FiniteMulArchimedeanClass.congrOrderIso e) a) = e ↑a

Defined in

Mathlib.Algebra.Order.Archimedean.Class

Cited by

0 results in Mathlib

Foundations

Depth 36 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommGroupLinearOrderIsOrderedMonoidCommGroupLinearOrderIsOrderedMonoid