Theorems · Definition · commutative algebra
MulOpposite.opLinearEquiv
(R : Type u) → {M : Type v} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → M ≃ₗ[R] MᵐᵒᵖThe function op is a linear equivalence.
- Defined in
- Mathlib.Algebra.Module.Equiv.Opposite
- Cited by
- 44 results in Mathlib
- Foundations
- Depth 23 from the axioms · uses propext, Quot.sound
- Assumes
- SemiringAddCommMonoidModule
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Modulestatement and proof · cited by 20,661
- RingHom.idstatement · cited by 18,349
- Semiringstatement and proof · cited by 13,802
- AddCommMonoidstatement and proof · cited by 12,281
- LinearEquivstatement · cited by 3,317
- MulOppositestatement and proof · cited by 1,135
- AddEquivproof · cited by 1,087
- Equiv.toFunproof · cited by 279
- AddEquiv.toEquivproof · cited by 174
- Equiv.invFunproof · cited by 163
- MulOpposite.opAddEquivproof · cited by 25
Cited by53
Results whose statement or proof uses this declaration.
- CliffordAlgebra.reverseproof · cited by 50
- CliffordAlgebra.reverseOpproof · cited by 11
- Submodule.equivOppositeproof · cited by 8
- Module.Basis.mulOppositeproof · cited by 7
- Algebra.TensorProduct.opAlgEquivproof · cited by 6
- MulOpposite.opLinearIsometryEquivproof · cited by 4
- MulOpposite.opContinuousLinearEquivproof · cited by 3
- Submodule.linearDisjoint_opproof · cited by 2
- Submodule.map_unop_mulstatement and proof · cited by 2
- CliffordAlgebra.reverseOp_ιproof · cited by 2
- CliffordAlgebra.submodule_map_pow_reverseproof · cited by 2
- rank_dual_eq_card_dual_of_aleph0_le_rank'proof · cited by 2