Theorem LinearMap.isOrthogonal_of_forall_apply_same

Modification history

2024-12-12 09:27

Mathlib/LinearAlgebra/SesquilinearForm.lean

refactor: make `LinearMap.IsAdjointPair` accept bare functions as arguments (#19679)

Modified LinearMap.isOrthogonal_of_forall_apply_same View on Github →

2024-09-18 09:37

Mathlib/LinearAlgebra/SesquilinearForm.lean

feat (LinearAlgebra/RootSystem) : Construct root systems from bilinear forms on reflexive modules (#16722) …

Added LinearMap.isOrthogonal_of_forall_apply_same View on Github →