Theorems · Theorem · number theory

QuadraticForm.toMatrix.congr_simp

∀ {R : Type u_3} {N : Type u_5} {n : Type w} [inst : Fintype n] {inst_1 : DecidableEq n} [inst_2 : DecidableEq n]
  [inst_3 : CommRing R] [inst_4 : Invertible 2] [inst_5 : AddCommGroup N] [inst_6 : Module R N]
  (b b_1 : Module.Basis n R N),
  b = b_1 →
    ∀ (Q Q_1 : QuadraticForm R N),
      Q = Q_1 →
        ∀ (a a_1 : n),
          a = a_1 →
            ∀ (a_2 a_3 : n), a_2 = a_3 → QuadraticForm.toMatrix b Q a a_2 = QuadraticForm.toMatrix b_1 Q_1 a_1 a_3

Defined in

Mathlib.LinearAlgebra.QuadraticForm.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

FintypeDecidableEqCommRingInvertibleAddCommGroupModule