Theorems · Theorem
Function.bijective_id
∀ {α : Sort u₁}, Function.Bijective id- Defined in
- Mathlib.Logic.Function.Defs
- Cited by
- 36 results in Mathlib
- Foundations
- Depth 4 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Function.Bijectivestatement · cited by 863
Cited by38
Results whose statement or proof uses this declaration.
- LinearMap.injective_of_comp_eq_idproof · cited by 9
- Set.ofPred_bijectiveproof · cited by 6
- LinearMap.surjective_of_comp_eq_idproof · cited by 5
- Module.End.isSemisimple_of_squarefree_aeval_eq_zeroproof · cited by 4
- Module.length_eq_of_surjectiveproof · cited by 4
- MulAction.isPreprimitive_stabilizer_of_surjectiveproof · cited by 2
- IsLocalization.of_le_isUnitproof · cited by 2
- IsHomeomorph.idproof · cited by 2
- Algebra.TensorProduct.includeLeft_bijectiveproof · cited by 2
- IsSemiprimaryRing.inductionproof · cited by 2
- Algebra.IsEffective.of_isEffective_tensorProduct_of_faithfullyFlatproof · cited by 1