Theorems · Theorem
Equiv.bijective
∀ {α : Sort u} {β : Sort v} (e : α ≃ β), Function.Bijective ⇑e- Defined in
- Mathlib.Logic.Equiv.Defs
- Cited by
- 132 results in Mathlib
- Foundations
- Depth 14 from the axioms, rests on 62 definitions · uses Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Equivstatement and proof · cited by 8,337
- Function.Bijectivestatement · cited by 863
- EquivLike.bijectiveproof · cited by 15
Cited by134
Results whose statement or proof uses this declaration.
- Matrix.det_mulproof · cited by 51
- LinearEquiv.bijectiveproof · cited by 35
- Fintype.sum_equivproof · cited by 35
- Fintype.prod_equivproof · cited by 18
- Fintype.ofEquiv_cardproof · cited by 16
- CategoryTheory.isIso_iff_bijectiveproof · cited by 16
- Fintype.ofEquivproof · cited by 15
- MulAction.bijectiveproof · cited by 11
- Matrix.submatrix_mul_equivproof · cited by 11
- CategoryTheory.bijective_iff_isIso_ofHomproof · cited by 8
- Equiv.preimage_eq_iff_eq_imageproof · cited by 8
- existsUnique_add_zsmul_mem_Iocproof · cited by 7