instSub

Mathlib.NumberTheory.ModularForms.SlashInvariantForms

URI: https://scilib.ai/kg/mathlib#SlashInvariantForm.instSub

English

There is a subtraction on SlashInvariantForm Γ k defined by f − g, compatible with the slash action.

Русский

Существует вычитание на SlashInvariantForm Γ k, задаваемое f − g и совместимое с слэш-акцией.

LaTeX

$$$$ (f - g)(z) = f(z) - g(z). $$$$

Lean4

instance instSub : Sub (SlashInvariantForm Γ k) :=
  ⟨fun f g => f + -g⟩

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

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

Разделы

Аффилиация

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