Mathlib Map

Theorems · Theorem · order theory

SetLike.coe_eq_coe

∀ {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p : A} {x y : ↥p}, ↑x = ↑y ↔ x = y
Defined in
Mathlib.Data.SetLike.Basic
Cited by
21 results in Mathlib
Foundations
Depth 8 from the axioms · uses no axioms
Assumes
SetLike
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Submodule.coe_eq_zero · cited by 9Submodule.coe_eq_zeroAddSubmonoid.mk_eq_zero · cited by 6AddSubmonoid.mk_eq_zeroSubMulAction.ofStabilizer.conjMap_bijective · cited by 2ofStabilizer.conjMap_bije…Equiv.Perm.isPretransitive_of_isCycle_mem · cited by 2Perm.isPretransitive_of_i…SubAddAction.ofStabilizer.addConjMap_bijective · cited by 2ofStabilizer.addConjMap_b…IsLocalization.integerMultiple_injective · cited by 2IsLocalization.integerMul…InfiniteGalois.restrictNormalHom_continuous · cited by 1InfiniteGalois.restrictNo…Valuation.ideal_isPrincipal · cited by 1Valuation.ideal_isPrincip…SubAddAction.addConjMap_ofFixingAddSubgroup_bijective · cited by 1SubAddAction.addConjMap_o…SubMulAction.ofFixingSubgroup_of_inclusion_injective · cited by 1SubMulAction.ofFixingSubg…MulAction.IsMultiplyPreprimitive.of_bijective_map · cited by 1IsMultiplyPreprimitive.of…SubAddAction.map_ofFixingAddSubgroupUnion_bijective · cited by 1SubAddAction.map_ofFixing…AddAction.IsMultiplyPreprimitive.of_bijective_map · cited by 1IsMultiplyPreprimitive.of…SubAddAction.stabilizer_of_subMul.addSubmonoid · cited by 1stabilizer_of_subMul.addS…HahnSeries.pow_add · cited by 0HahnSeries.pow_addSetLike · cited by 1084SetLikeSetLike.coe_eq_coeCITED 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 by21

Results whose statement or proof uses this declaration.