instMulArchimedean — Mathlib

English

MulArchimedean on WithZero M follows from MulArchimedean on M.

Русский

MulArchimedean на WithZero M следует из MulArchimedean на M.

LaTeX

$$$$ \text{MulArchimedean}(M) \Rightarrow \text{MulArchimedean}(WithZero M). $$$$

Lean4

instance instMulArchimedean (M) [CommMonoid M] [PartialOrder M] [MulArchimedean M] : MulArchimedean (WithZero M) :=
  by
  constructor
  intro x y hxy
  cases y with
  | zero => exact absurd hxy (zero_le _).not_gt
  | coe y =>
    cases x with
    | zero => refine ⟨0, zero_le _⟩
    | coe x => simpa [← WithZero.coe_pow] using (MulArchimedean.arch x (by simpa using hxy))

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