Theorems · Theorem · commutative algebra
OrzechProperty.injective_of_surjective_of_injective
∀ {R : Type u} [inst : Semiring R] [OrzechProperty R] {M : Type v} [inst_2 : AddCommMonoid M] [inst_3 : Module R M]
[Module.Finite R M] {N : Type w} [inst_5 : AddCommMonoid N] [inst_6 : Module R N] (i f : N →ₗ[R] M),
Function.Injective ⇑i → Function.Surjective ⇑f → Function.Injective ⇑f- Defined in
- Mathlib.RingTheory.OrzechProperty
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 91 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites25
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Modulestatement and proof · cited by 20,661
- RingHom.idstatement and proof · cited by 18,349
- Semiringstatement and proof · cited by 13,802
- AddCommMonoidstatement and proof · cited by 12,281
- LinearMapstatement and proof · cited by 10,215
- Equiv.symmproof · cited by 3,681
- LinearEquivproof · cited by 3,317
- LinearMap.compproof · cited by 1,642
- LinearEquiv.symmproof · cited by 1,461
- LinearEquiv.toLinearMapproof · cited by 1,171
- Module.Finitestatement and proof · cited by 1,032
Cited by5
Results whose statement or proof uses this declaration.
- Subalgebra.LinearDisjoint.of_finrank_sup_of_freeproof · cited by 2
- OrzechProperty.injective_of_surjective_endomorphismproof · cited by 1
- linearIndependent_of_top_le_span_of_card_le_finrankproof · cited by 1
- OrzechProperty.bijective_of_surjective_of_injectiveproof · cited by 1
- OrzechProperty.injective_of_surjective_of_submoduleproof · cited by 0