Theorems · Theorem · ring theory

QuadraticAlgebra.omega_mul_algebraMap_mul_mk

∀ {R : Type u_2} {a b : R} [inst : CommSemiring R] (n x y : R),
  QuadraticAlgebra.omega * (algebraMap R (QuadraticAlgebra R a b)) n * { re := x, im := y } =
    { re := a * n * y, im := n * x + n * b * y }

Defined in

Mathlib.Algebra.QuadraticAlgebra.Basic

Cited by

0 results in Mathlib

Foundations

Depth 32 from the axioms · uses propext, Quot.sound

Assumes

CommSemiring