linearEquivOp — Mathlib

English

There is a natural linear equivalence between a subalgebra S and its opposite: S ≃ₗ[R] S^{op}.

Русский

Существует естественное линейное эквивалентность между подалгеброй S и её противоположностью: S ≃ₗ[R] S^{op}.

LaTeX

$$$$S \\cong_R S^{op}$$$$

Lean4

/-- Bijection between a subalgebra `S` and its opposite. -/
@[simps!]
def linearEquivOp (S : Subalgebra R A) : S ≃ₗ[R] S.op
    where
  __ := S.toSubsemiring.addEquivOp
  map_smul' _ _ := rfl

Похожие утверждения