Theorems · Theorem · ring theory
RingEquiv.bijective
∀ {R : Type u_4} {S : Type u_5} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] (e : R ≃+* S),
Function.Bijective ⇑e- Defined in
- Mathlib.Algebra.Ring.Equiv
- Cited by
- 22 results in Mathlib
- Foundations
- Depth 17 from the axioms · 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
- RingEquivstatement and proof · cited by 1,147
- Function.Bijectivestatement · cited by 863
- EquivLike.bijectiveproof · cited by 15
Cited by22
Results whose statement or proof uses this declaration.
- RingHom.LocalizationAwayPreserves.respectsIsoproof · cited by 4
- Algebra.lift_rank_eq_of_equiv_equivproof · cited by 4
- RingHom.FormallySmooth.respectsIsoproof · cited by 3
- AlgebraicIndependent.option_iff_transcendentalproof · cited by 3
- RingHom.injective_respectsIsoproof · cited by 2
- RingHom.Flat.comp_iff_of_bijective_rightproof · cited by 2
- WittVector.frobenius_bijectiveproof · cited by 2
- RingHom.IsStandardSmoothOfRelativeDimension.equivproof · cited by 2
- RingHom.StableUnderCompositionWithLocalizationAway.respectsIsoproof · cited by 1
- RingHom.Flat.comp_iff_of_bijective_leftproof · cited by 1
- RingHom.Flat.respectsIsoproof · cited by 1
- MaximalSpectrum.mapPiLocalization_bijectiveproof · cited by 1