Def RootPairing.Hom.id

Modification history

2024-10-31 02:17

Mathlib/LinearAlgebra/RootSystem/Hom.lean

feat (RootSystem/Hom): endomorphisms and automorphisms of root pairings (#18025) …

Modified RootPairing.Hom.id View on Github →

2024-09-09 08:37

Mathlib/LinearAlgebra/RootSystem/Hom.lean

feat (LinearAlgebra/RootPairing): define RootPairingCat (#16295) …

Added RootPairing.Hom.id View on Github →