reduceStep

Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

URI: https://scilib.ai/kg/mathlib#FixedDetMatrices.reduceStep

← MathLib Explorer

English

A single reduction step is defined as above: reduceStep(A) = S • (T^( -(A_00 / A_10))) • A.

Русский

Один шаг редукции: reduceStep(A) = S • T^{-(A_{00}/A_{10})} • A.

LaTeX

$$$\text{reduceStep}(A) = S \cdot T^{-(A_{00}/A_{10})} \cdot A$.$$

Lean4

/-- Reduction step for matrices in `Δ m` which moves the matrices towards `reps` -/
def reduceStep (A : Δ m) : Δ m :=
  S • (T ^ (-(A.1 0 0 / A.1 1 0))) • A

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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