English
Linear disjointness is preserved by taking multiplicative opposite: M linearDisjoint N if and only if the corresponding opposite submodules are linearly disjoint after applying equivalences.
Русский
Линейная несовместность сохраняется при переходе к мультипликативному противоположному: M ⟂_R N эквивалентно их противоположностям после применения соответствующих эквив.
LaTeX
$$$M.LinearDisjoint N \iff (equivOpposite.symm (MulOpposite.op N)).LinearDisjoint (equivOpposite.symm (MulOpposite.op M))$$$
Lean4
/-- Linear disjointness is preserved by taking multiplicative opposite. -/
theorem linearDisjoint_op :
M.LinearDisjoint N ↔
(equivOpposite.symm (MulOpposite.op N)).LinearDisjoint (equivOpposite.symm (MulOpposite.op M)) :=
by
simp only [linearDisjoint_iff, mulMap_op, LinearMap.coe_comp, LinearEquiv.coe_coe, EquivLike.comp_injective,
EquivLike.injective_comp]
