congr_apply

Mathlib.RingTheory.AdicCompletion.Functoriality

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

English

Equality of linear equivalences with map on adic completion aligns with congr I f x.

Русский

Согласование применений линейного эквивалента через AdicCompletion.

LaTeX

$$$\forall (f : M \simeq N), (x : AdicCompletion I M), congr I f x = map I f x$$$

Lean4

@[simp]
theorem congr_apply (f : M ≃ₗ[R] N) (x : AdicCompletion I M) : congr I f x = map I f x :=
  rfl

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

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

Разделы

Аффилиация

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