Theorems · Theorem · number theory

QuadraticMap.linMulLin_comp

∀ {R : Type u_3} {M : Type u_4} {A : Type u_7} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Module R M] [inst_4 : Module R A] [inst_5 : SMulCommClass R A A]
  [inst_6 : IsScalarTower R A A] {N' : Type u_8} [inst_7 : AddCommMonoid N'] [inst_8 : Module R N'] (f g : M →ₗ[R] A)
  (h : N' →ₗ[R] M), (QuadraticMap.linMulLin f g).comp h = QuadraticMap.linMulLin (f ∘ₗ h) (g ∘ₗ h)

Defined in

Mathlib.LinearAlgebra.QuadraticForm.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringNonUnitalNonAssocSemiringAddCommMonoidModuleModuleSMulCommClassIsScalarTowerAddCommMonoidModule