mem_prod

Mathlib.RingTheory.Ideal.Prod

URI: https://scilib.ai/kg/mathlib#Ideal.mem_prod

English

For x = (r,s) ∈ R × S, x ∈ prod I J iff r ∈ I and s ∈ J.

Русский

Для x = (r,s) ∈ R × S верно: x ∈ prod I J тогда и только тогда r ∈ I и s ∈ J.

LaTeX

$$x \in I.prod J \iff x.fst \in I \land x.snd \in J$$

Lean4

@[simp]
theorem mem_prod {x : R × S} : x ∈ prod I J ↔ x.1 ∈ I ∧ x.2 ∈ J :=
  Iff.rfl

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

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

Разделы

Аффилиация

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