Action on flags

Order isomorphisms act on flags.

instance Flag.instSMulOrderIso {α : Type u_1} [Preorder α] : SMul (α ≃o α) (Flag α)

Equations

• Flag.instSMulOrderIso = { smul := fun (e : α ≃o α) => ⇑(Flag.map e) }

@[simp]

theorem Flag.coe_smul {α : Type u_1} [Preorder α] (e : α ≃o α) (s : Flag α) : ↑(e • s) = e • ↑s

instance Flag.instMulActionOrderIso {α : Type u_1} [Preorder α] : MulAction (α ≃o α) (Flag α)

Equations

• Flag.instMulActionOrderIso = Function.Injective.mulAction SetLike.coe ⋯ ⋯