Commit 2024-09-09 08:37 eac55c09
View on Github →feat (LinearAlgebra/RootPairing): define RootPairingCat (#16295) This PR defines a category of root pairings, roughly following the treatment of morphisms of root data in SGA3 Exp.21 Sec.6.
feat (LinearAlgebra/RootPairing): define RootPairingCat (#16295) This PR defines a category of root pairings, roughly following the treatment of morphisms of root data in SGA3 Exp.21 Sec.6.