Theorem nontrivial_of_hasRankNullity

Modification history

2026-10-10 13:11

Mathlib/LinearAlgebra/Dimension/RankNullity.lean

feat(LinearAlgebra): make two `Nontrivial` theorems low priority instances (#44558) …

Modified nontrivial_of_hasRankNullity View on Github →

2024-07-14 23:18

Mathlib/LinearAlgebra/Dimension/RankNullity.lean

chore (LinearAlgebra.Dimension): make `instNontrivial` a local instance (#14120) …

Added nontrivial_of_hasRankNullity View on Github →