English
The smul action is faithful on the subtype of adic completion integers.
Русский
Действие умножения является инъективным на подмножество целых adic завершения.
LaTeX
$$instFaithfulSMulSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers$$
Lean4
instance : Algebra R (v.adicCompletionIntegers K)
where
smul r
x :=
⟨r • (x : v.adicCompletion K),
by
have h : (algebraMap R (adicCompletion K v)) r = (algebraMap R K r : adicCompletion K v) := rfl
rw [Algebra.smul_def]
refine ValuationSubring.mul_mem _ _ _ ?_ x.2
rw [h]
exact coe_algebraMap_mem _ _ v r⟩
algebraMap :=
{ toFun r := ⟨(algebraMap R K r : adicCompletion K v), coe_algebraMap_mem _ _ v r⟩
map_one' := by simp only [map_one]; rfl
map_mul' x
y := by
ext
simp only [map_mul, UniformSpace.Completion.coe_mul, MulMemClass.mk_mul_mk]
map_zero' := by simp only [map_zero]; rfl
map_add' x
y := by
ext
simp only [map_add, UniformSpace.Completion.coe_add, AddMemClass.mk_add_mk] }
commutes' r x := by rw [mul_comm]
smul_def' r
x := by
ext
simp only [Algebra.smul_def]
rfl
