Theorem AlternatingMap.domDomCongrₗ_toAddEquiv

Modification history

2023-11-29 19:54
Mathlib/LinearAlgebra/Alternating/Basic.lean
chore: introduce notation for `AlternatingMap` (#8697) …
Added AlternatingMap.domDomCongrₗ_toAddEquivView on Github →