lcRow0_apply

Mathlib.NumberTheory.Modular

URI: https://scilib.ai/kg/mathlib#ModularGroup.lcRow0_apply

English

For p=(c,d) and a matrix g = [[a,b],[c,d]] the value lcRow0 p g equals c⋅a + d⋅b.

Русский

Пусть p=(c,d) и матрица g=[[a,b],[c,d]]; тогда lcRow0(p)g = c·a + d·b.

LaTeX

$$$lcRow0(p)g = p_0 \\cdot g_{00} + p_1 \\cdot g_{01}.$$$

Lean4

@[simp]
theorem lcRow0_apply (p : Fin 2 → ℤ) (g : Matrix (Fin 2) (Fin 2) ℝ) : lcRow0 p g = p 0 * g 0 0 + p 1 * g 0 1 :=
  rfl

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

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

Разделы

Аффилиация

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