def StandardRepr.dual {α R : Type} [DecidableEq α] [Ring R] (S : StandardRepr α R) : StandardRepr α R

The dual of standard representation (transpose the matrix and flip its signs).

Equations

• S✶ = { X := S.Y, Y := S.X, hXY := ⋯, B := -S.B.transpose, decmemX := S.decmemY, decmemY := S.decmemX }

def «term_✶» : Lean.TrailingParserDescr

Equations

• «term_✶» = Lean.ParserDescr.trailingNode `«term_✶» 1024 1024 (Lean.ParserDescr.symbol "✶")

theorem StandardRepr.dual_toMatroid {α R : Type} [DecidableEq α] [Ring R] (S : StandardRepr α R) : S✶.toMatroid = S.toMatroid✶

The dual of standard representation gives a dual matroid.

theorem VectorMatroid.dual_exists_standardRepr {α R : Type} [DecidableEq α] [Ring R] (M : VectorMatroid α R) : ∃ (S' : StandardRepr α R), S'.toMatroid = M.toMatroid✶

Every vector matroid's dual has a standard representation.