completion_zero — Mathlib

English

The completion of the zero homomorphism is the zero homomorphism.

Русский

Дополнение нулевого гомоморфизма равно нулевому гомоморфизму.

LaTeX

$$$\\text{completion}(0) = 0$$$

Lean4

theorem completion_zero : AddMonoidHom.completion (0 : α →+ β) continuous_const = 0 :=
  by
  ext x
  refine Completion.induction_on x ?_ ?_
  · apply isClosed_eq (AddMonoidHom.continuous_completion (0 : α →+ β) continuous_const)
    exact continuous_const
  · simp [(0 : α →+ β).completion_coe continuous_const, coe_zero]

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