Theorems · Theorem · category theory

QuadraticModuleCat.ofIso_symm

∀ {R : Type u} [inst : CommRing R] {X Y : Type v} [inst_1 : AddCommGroup X] [inst_2 : Module R X]
  [inst_3 : AddCommGroup Y] [inst_4 : Module R Y] {Q₁ : QuadraticForm R X} {Q₂ : QuadraticForm R Y}
  (e : QuadraticMap.IsometryEquiv Q₁ Q₂), QuadraticModuleCat.ofIso e.symm = (QuadraticModuleCat.ofIso e).symm

Defined in

Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModuleAddCommGroupModule