Def QuadraticModuleCat.of

Modification history

2025-02-05 23:58
Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat.lean
refactor(LinearAlgebra): `ConcreteCategory` instance for `QuadraticModuleCat` (#21471) …
Deleted QuadraticModuleCat.ofView on Github →
2023-09-18 15:32
Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat.lean
feat: the category of quadratic modules, QuadraticModuleCat (#6987) …
Added QuadraticModuleCat.ofView on Github →