Theorem LinearMap.IsAlt.ortho_comm

Modification history

2024-08-01 00:14

Mathlib/LinearAlgebra/SesquilinearForm.lean

chore: robustifying for debug.byAsSorry (part 14) (#15247)

Modified LinearMap.IsAlt.ortho_comm View on Github →

2023-03-22 14:30

Mathlib/LinearAlgebra/SesquilinearForm.lean

feat: port LinearAlgebra.SesquilinearForm (#2607)

Added LinearMap.IsAlt.ortho_comm View on Github →