Theorems · Theorem · category theory
LinearMap.exact_subtype_mkQ
∀ {R : Type u_8} {N : Type u_10} [inst : Ring R] [inst_1 : AddCommGroup N] [inst_2 : Module R N] (Q : Submodule R N),
Function.Exact ⇑Q.subtype ⇑Q.mkQ- Defined in
- Mathlib.Algebra.Exact.Basic
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 86 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- RingAddCommGroupModule
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Modulestatement and proof · cited by 20,661
- RingHom.idstatement · cited by 18,349
- AddCommGroupstatement and proof · cited by 12,871
- LinearMapstatement · cited by 10,215
- Ringstatement and proof · cited by 7,463
- Submodulestatement and proof · cited by 7,192
- HasQuotient.Quotientstatement · cited by 2,301
- LinearMap.rangeproof · cited by 893
- Submodule.subtypestatement and proof · cited by 480
- Submodule.mkQstatement · cited by 232
- Function.Exactstatement · cited by 182
Cited by10
Results whose statement or proof uses this declaration.
- Module.Flat.exists_factorization_of_finitePresentationproof · cited by 2
- Ideal.subtype_rTensor_rangeproof · cited by 1
- rTensor_mkQproof · cited by 1
- Module.exists_basis_of_basis_baseChangeproof · cited by 1
- IsLocalRing.split_injective_iff_lTensor_residueField_injectiveproof · cited by 1
- IsNoetherianRing.induction_on_isQuotientEquivQuotientPrimeproof · cited by 1
- Module.free_of_lTensor_residueField_injectiveproof · cited by 1
- lTensor_mkQproof · cited by 1
- Module.Finite.of_submodule_quotientproof · cited by 0
- Submodule.isCoideal_iff_comul_memproof · cited by 0