sub

Mathlib.RingTheory.Congruence.Defs

URI: https://scilib.ai/kg/mathlib#RingCon.sub

← MathLib Explorer

English

If a ≡ b and c ≡ d, then a − c ≡ b − d.

Русский

Если a конгруэнт b и c конгруэнт d, то a − c конгруэнт b − d.

LaTeX

$$$$\forall a b c d,\ t a b \Rightarrow t c d \Rightarrow t (a - c) (b - d).$$$$

Lean4

protected theorem sub {S : Type*} [AddGroup S] [Mul S] (t : RingCon S) {a b c d : S} (h : t a b) (h' : t c d) :
    t (a - c) (b - d) :=
  t.toAddCon.sub h h'

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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