Mathlib Map

Theorems · Theorem · order theory

SetLike.coe_mem

∀ {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p : A} (x : ↥p), ↑x ∈ p
Defined in
Mathlib.Data.SetLike.Basic
Cited by
46 results in Mathlib
Foundations
Depth 5 from the axioms · uses no axioms
Assumes
SetLike
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

IsIntegralClosure.isLocalization · cited by 13IsIntegralClosure.isLocal…OreLocalization.expand' · cited by 3OreLocalization.expand'Ideal.IsHomogeneous.isPrime_of_homogeneous_mem_or_mem · cited by 3IsHomogeneous.isPrime_of_…AddSubgroup.leftCoset_cover_filter_FiniteIndex_aux · cited by 3AddSubgroup.leftCoset_cov…Ideal.absNorm_ne_zero_of_nonZeroDivisors · cited by 3Ideal.absNorm_ne_zero_of_…Submodule.projection_apply_mem · cited by 3Submodule.projection_appl…ZLattice.covolume_div_covolume_eq_relIndex · cited by 2ZLattice.covolume_div_cov…EuclideanGeometry.orthogonalProjection_affineSpan_singleton · cited by 2EuclideanGeometry.orthogo…NumberField.IsCMField.RingOfIntegers.complexConj_eq_self_iff · cited by 2RingOfIntegers.complexCon…lieModule_lcs_map_le · cited by 2lieModule_lcs_map_leAffineSubspace.signedInfDist_eq_signedDist_of_mem · cited by 2AffineSubspace.signedInfD…AddSubgroup.relIndex_eq_natAbs_det · cited by 2AddSubgroup.relIndex_eq_n…Ideal.absNorm_pos_of_nonZeroDivisors · cited by 2Ideal.absNorm_pos_of_nonZ…NumberField.Units.closure_fundSystem_sup_torsion_eq_top · cited by 2Units.closure_fundSystem_…FractionalIdeal.zero_of_num_eq_bot · cited by 2FractionalIdeal.zero_of_n…SetLike · cited by 1084SetLikeSetLike.coe_memCITED BYCITES

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • SetLikestatement and proof · cited by 1,084

Cited by46

Results whose statement or proof uses this declaration.