English
LinearEquivClass F R M M₂ asserts that F is a class of bundled R-linear equivalences between M and M₂; this is an abbreviation for the SemilinearEquivClass with ring identity.
Русский
LinearEquivClass F R M M₂ утверждает, что F — класс объединённых R-линейных эквивалентностей между M и M₂; это сокращение для SemilinearEquivClass с тождественным кольцом.
LaTeX
$$$ \text{LinearEquivClass}(F,R,M,M_2) \equiv \text{SemilinearEquivClass}(F, \mathrm{id}_R, M, M_2) $$$
Lean4
/-- `LinearEquivClass F R M M₂` asserts `F` is a type of bundled `R`-linear equivs `M → M₂`.
This is an abbreviation for `SemilinearEquivClass F (RingHom.id R) M M₂`.
-/
abbrev LinearEquivClass (F : Type*) (R M M₂ : outParam Type*) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂]
[Module R M] [Module R M₂] [EquivLike F M M₂] :=
SemilinearEquivClass F (RingHom.id R) M M₂
