Mathlib Map

Theorems · Theorem

EquivLike.injective

∀ {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} [inst : EquivLike E α β] (e : E), Function.Injective ⇑e
Defined in
Mathlib.Data.FunLike.Equiv
Cited by
32 results in Mathlib
Foundations
Depth 10 from the axioms · uses Quot.sound
Assumes
EquivLike
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Equiv.injective · cited by 464Equiv.injectiveAlgEquiv.injective · cited by 61AlgEquiv.injectiveAddEquiv.injective · cited by 58AddEquiv.injectiveRingEquiv.injective · cited by 39RingEquiv.injectiveMulEquiv.injective · cited by 36MulEquiv.injectiveEquivLike.bijective · cited by 15EquivLike.bijectivedualTensorHom_bijective · cited by 6dualTensorHom_bijectiveFirstOrder.Language.Equiv.injective · cited by 4Equiv.injectiveAddEquiv.map_finsum · cited by 3AddEquiv.map_finsumisAlgebraic_ringHom_iff_of_comp_eq · cited by 3isAlgebraic_ringHom_iff_o…MulEquiv.map_finprod · cited by 2MulEquiv.map_finprodIsAdjoinRootMonic.ext_elem · cited by 2IsAdjoinRootMonic.ext_elemmap_eq_bot_iff · cited by 1map_eq_bot_iffAlgebra.isAlgebraic_ringHom_iff_of_comp_eq · cited by 1Algebra.isAlgebraic_ringH…map_eq_top_iff · cited by 1map_eq_top_iffDFunLike.coe · cited by 62936DFunLike.coeEquivLike · cited by 165EquivLikeEmbeddingLike.injective · cited by 14EmbeddingLike.injectiveEquivLike.injectiveCITED BYCITES

Cites3

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

Cited by32

Results whose statement or proof uses this declaration.