coe_sumSq — Mathlib

English

In a NonUnitalSubsemiring, sumSq T is exactly the set of elements with IsSumSq, i.e., sumSq T = { s : T | IsSumSq s }.

Русский

В NonUnitalSubsemiring сумма квадратов равна множеству элементов, удовлетворяющих IsSumSq: sumSq T = { s : T | IsSumSq s }.

LaTeX

$$$\operatorname{sumSq}\ T = \{ s : T \mid \operatorname{IsSumSq}(s) \}$$$

Lean4

@[simp, norm_cast]
theorem coe_sumSq : sumSq T = {s : T | IsSumSq s} := by ext; simp

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