Theorem SymplecticGroup.mem_iff'

Modification history

2023-08-16 09:33

Mathlib/LinearAlgebra/SymplecticGroup.lean

refactor(Data/Matrix): Eliminate `⬝` notation in favor of `HMul` (#6487) …

Modified SymplecticGroup.mem_iff'View on Github →

2023-04-29 03:33

Mathlib/LinearAlgebra/SymplecticGroup.lean

feat: port LinearAlgebra.SymplecticGroup (#3696)

Added SymplecticGroup.mem_iff'View on Github →