instLocallyFiniteOrderMultiplicative

English

If X has a locally finite order, then Multiplicative X also carries a locally finite order, transported via the natural isomorphism to X.

Русский

Если у X локально конечный порядок, то и Multiplicative X имеет локально конечный порядок, перенесенный через естественный изоморфизм на X.

LaTeX

$$$\text{LocallyFiniteOrder}(\mathrm{Multiplicative}(X))$$$

Lean4

instance : LocallyFiniteOrder (Multiplicative X) :=
  OrderIso.locallyFiniteOrder (⟨Multiplicative.toAdd, by simp⟩ : Multiplicative X ≃o X)

Похожие утверждения