instFaithfulSMulSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers

English

There is a faithful smul structure on the subtype of adic completion integers.

Русский

Существует корректная структура умножения на подтип целых adic завершения.

LaTeX

$$instFaithfulSMulSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers$$

Lean4

instance [FaithfulSMul R K] : FaithfulSMul R (v.adicCompletionIntegers K) :=
  by
  rw [faithfulSMul_iff_algebraMap_injective]
  intro x y
  simp [Subtype.ext_iff, (FaithfulSMul.algebraMap_injective R K).eq_iff]

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