Mathlib v3 is deprecated. Go to Mathlib v4

Def submodule.gi_map_comap

Modification history

2021-09-04 08:16

src/linear_algebra/basic.lean

feat(linear_algebra/basic): galois insertion lemmas for map and comap (#8978)

Added submodule.gi_map_comap View on Github →