Theorems · Theorem · group theory
SMulCommClass.symm
∀ (M : Type u_9) (N : Type u_10) (α : Type u_11) [inst : SMul M α] [inst_1 : SMul N α] [SMulCommClass M N α], SMulCommClass N M α
Commutativity of actions is a symmetric relation. This lemma can't be an instance because this would cause a loop in the instance search graph.
- Defined in
- Mathlib.Algebra.Group.Action.Defs
- Cited by
- 67 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
- Assumes
- SMulSMulSMulCommClass
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- SMulCommClassstatement and proof · cited by 1,927
- SMulCommClass.smul_commproof · cited by 143
Cited by81
Results whose statement or proof uses this declaration.
- LinearMap.flipstatement · cited by 193
- smul_mul_smul_commproof · cited by 14
- LinearMap.finsuppLinearMapproof · cited by 7
- RootPairing.coroot_root_twostatement · cited by 7
- LinearMap.lflipstatement · cited by 6
- RootPairing.flip_toLinearMapstatement · cited by 4
- flip_innerₗstatement · cited by 4
- RootPairing.equiv_of_mapsTostatement · cited by 3
- Coalgebra.lTensor_counit_comp_comulstatement · cited by 3
- LinearMap.separatingRight_iff_flip_ker_eq_botstatement · cited by 3
- Algebra.FormallyUnramified.comp_secstatement · cited by 3
- Submodule.flip_quotDualCoannihilatorToDual_injectivestatement · cited by 3