map_zero

Mathlib.RingTheory.AdicCompletion.Functoriality

URI: https://scilib.ai/kg/mathlib#AdicCompletion.map_zero

English

Equality of congr I f x and map I f x holds; i.e., congr I f x = map I f x.

Русский

Равенство congr I f x и map I f x.

LaTeX

$$$\text{congr } I f\ x = \mathrm{map}\ I f\ x$$$

Lean4

@[simp]
theorem map_zero : map I (0 : M →ₗ[R] N) = 0 := by
  ext
  simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru