Theorems · Theorem · general topology

Matrix.mulVec_fin_two

∀ {R : Type u_1} [inst : Semiring R] (m : Matrix (Fin 2) (Fin 2) R) (v : Fin 2 → R),
  m.mulVec v = ![m 0 0 * v 0 + m 0 1 * v 1, m 1 0 * v 0 + m 1 1 * v 1]

Defined in

Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Cited by

1 results in Mathlib

Foundations

Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Semiring