Mathlib Map

Theorems · Theorem · commutative algebra

Submodule.neg_mem_iff

∀ {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
11 results in Mathlib
Foundations
Depth 18 from the axioms · uses propext
Assumes
RingAddCommGroup
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Submodule.sub_mem_iff_right · cited by 4Submodule.sub_mem_iff_rig…Submodule.neg_eq_self · cited by 3Submodule.neg_eq_selfEuclideanGeometry.orthogonalProjection_mem_orthogonal · cited by 3EuclideanGeometry.orthogo…iSupIndep_iff_finsetSum_eq_zero_imp_eq_zero · cited by 3iSupIndep_iff_finsetSum_e…LinearMap.BilinForm.exists_orthogonal_basis · cited by 2BilinForm.exists_orthogon…Ideal.neg_mem_iff · cited by 2Ideal.neg_mem_iffrange_mvfderiv_subtypeVal · cited by 1range_mvfderiv_subtypeValAffineSubspace.coe_direction_eq_vsub_set_left · cited by 1AffineSubspace.coe_direct…EuclideanGeometry.Sphere.orthogonalProjection_orthRadius_center · cited by 0Sphere.orthogonalProjecti…Algebra.Extension.Cotangent.map_ker_of_surjective · cited by 0Cotangent.map_ker_of_surj…Submodule.neg_coe · cited by 0Submodule.neg_coeModule · cited by 20661ModuleAddCommGroup · cited by 12871AddCommGroupRing · cited by 7463RingSubmodule · cited by 7192Submoduleneg_mem_iff · cited by 42neg_mem_iffSubmodule.neg_mem_iffCITED BYCITES

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
  • neg_mem_iffproof · cited by 42

Cited by11

Results whose statement or proof uses this declaration.