Theorems · Theorem · number theory

QuadraticMap.weightedSumSquares.congr_simp

∀ {S : Type u_1} (R : Type u_3) [inst : CommSemiring R] {ι : Type u_8} [inst_1 : Fintype ι] [inst_2 : Monoid S]
  [inst_3 : DistribMulAction S R] [inst_4 : SMulCommClass S R R] (w w_1 : ι → S),
  w = w_1 → QuadraticMap.weightedSumSquares R w = QuadraticMap.weightedSumSquares R w_1

Defined in: Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
Cited by: 0 results in Mathlib
Foundations: Depth 47 from the axioms · uses propext, Quot.sound
Assumes: CommSemiring Fintype Monoid DistribMulAction SMulCommClass

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CommSemiringstatement and proof · cited by 10,911
Fintypestatement and proof · cited by 7,736
Monoidstatement and proof · cited by 3,887
SMulCommClassstatement and proof · cited by 1,927
DistribMulActionstatement and proof · cited by 584
QuadraticMapstatement · cited by 262
QuadraticMap.weightedSumSquaresstatement and proof · cited by 18

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.