coe_copy

Mathlib.RingTheory.NonUnitalSubring.Defs

URI: https://scilib.ai/kg/mathlib#NonUnitalSubring.coe_copy

English

The underlying set of S.copy s hs is precisely s.

Русский

Преобразování носителя S.copy s hs дает множество, равное s.

LaTeX

$$$(S.copy\, s\, hs : Set R) = s$$$

Lean4

@[simp]
theorem coe_copy (S : NonUnitalSubring R) (s : Set R) (hs : s = ↑S) : (S.copy s hs : Set R) = s :=
  rfl

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

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

Разделы

Аффилиация

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