Documentation

Mathlib.Algebra.Order.Group.Action.Flag

Action on flags #

Order isomorphisms act on flags.

source
instance Flag.instSMulOrderIso {α : Type u_1} [Preorder α] :
SMul (α ≃o α) (Flag α)
Equations
    source
    @[simp]
    theorem Flag.coe_smul {α : Type u_1} [Preorder α] (e : α ≃o α) (s : Flag α) :
    ↑(e • s) = e • ↑s
    source
    instance Flag.instMulActionOrderIso {α : Type u_1} [Preorder α] :
    MulAction (α ≃o α) (Flag α)
    Equations