Structures · Algebra

SemilinearEquivClass

SemilinearEquivClass F σ M M₂ asserts F is a type of bundled σ-semilinear equivs M → M₂. See also LinearEquivClass F R M M₂ for the case where σ is the identity map on R. A map f between an R-module and an S-module over a ring homomorphism σ : R →+* S is semilinear if it satisfies the two properties f (x + y) = f x + f y and f (c • x) = (σ c) • f x.

Defined in

Mathlib.Algebra.Module.Equiv.Defs

Shape

4 explicit arguments · adds map_smulₛₗ