Mathlib Map

Structures · Algebra

MulSemiringActionSemiHomClass

MulSemiringActionHomClass F φ R S states that F is a type of morphisms preserving the ring structure and equivariant with respect to φ. You should extend this class when you extend MulSemiringActionHom.

Defined in
Mathlib.GroupTheory.GroupAction.Hom
Shape
4 explicit arguments

Extends2

Extended by0

Nothing extends this class yet.

Concrete types that are instances1

  • MulSemiringActionHom

How is a type an instance?

Loading the hierarchy index…

Assumed by5

Ancestors10