σ

Mathlib.RingTheory.Extension.Generators

URI: https://scilib.ai/kg/mathlib#Algebra.Generators.Simps.σ

English

The Simps projection for σ is simply the σ-map from S to P.Ring, kept for convenience in simps tooling.

Русский

Проекция Simps для σ проста: σ-маршрут из S в P.Ring, сохранённый для удобства скриптов Simps.

LaTeX

$$def σ : S → P.Ring := P.σ$$

Lean4

/-- See Note [custom simps projection] -/
def σ : S → P.Ring :=
  P.σ

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

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

Разделы

Аффилиация

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