Theorems · Theorem · commutative algebra
Submodule.neg_mem
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] {module_M : Module R M} (p : Submodule R M)
{x : M}, x ∈ p → -x ∈ p- Defined in
- Mathlib.Algebra.Module.Submodule.Defs
- Cited by
- 31 results in Mathlib
- Foundations
- Depth 18 from the axioms · uses propext
- Assumes
- RingAddCommGroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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
- AddCommGroupstatement and proof · cited by 12,871
- Ringstatement and proof · cited by 7,463
- Submodulestatement and proof · cited by 7,192
- NegMemClass.neg_memproof · cited by 63
Cited by32
Results whose statement or proof uses this declaration.
- Submodule.toAddSubgroupproof · cited by 106
- Submodule.fg_iff_addSubgroup_fgproof · cited by 3
- Submodule.eq_smul_of_le_smul_of_le_jacobsonproof · cited by 3
- iSupIndep_iff_finsetSum_eq_zero_imp_eq_zeroproof · cited by 3
- AffineSubspace.vadd_mem_iff_mem_of_mem_directionproof · cited by 3
- AffineSubspace.wOppSide_vadd_left_iffproof · cited by 2
- AffineSubspace.wSameSide_vadd_left_iffproof · cited by 2
- Ideal.mem_jacobson_iffproof · cited by 2
- Ideal.Quotient.ker_stabilizerHomproof · cited by 2
- Submodule.sub_mem_iff_leftproof · cited by 2
- Submodule.exists_mem_and_smul_eq_self_of_fg_of_le_smulproof · cited by 2
- LieAlgebra.IsKilling.mem_rootSet_invtSubmoduleToLieIdealproof · cited by 2