Theorems · Theorem · field theory
RatFunc.liftMonoidWithZeroHom_injective
∀ {G₀ : Type u_1} {R : Type u_3} [inst : CommGroupWithZero G₀] [inst_1 : CommRing R] [Nontrivial R]
(φ : Polynomial R →*₀ G₀) (hφ : Function.Injective ⇑φ)
(hφ' : optParam (nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors G₀)) ⋯),
Function.Injective ⇑(RatFunc.liftMonoidWithZeroHom φ hφ')- Defined in
- Mathlib.FieldTheory.RatFunc.Basic
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 111 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites24
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
- CommRingstatement and proof · cited by 17,173
- Polynomialstatement and proof · cited by 5,681
- Submonoidstatement · cited by 3,086
- Nontrivialstatement and proof · cited by 2,416
- mul_commproof · cited by 2,262
- map_mulproof · cited by 1,137
- nonZeroDivisorsstatement and proof · cited by 895
- MonoidWithZeroHomstatement and proof · cited by 704
- RatFuncstatement and proof · cited by 301
- FractionRingproof · cited by 200
- Submonoid.comapstatement and proof · cited by 179
Cited by2
Results whose statement or proof uses this declaration.
- RatFunc.liftRingHom_injectiveproof · cited by 0
- RatFunc.liftAlgHom_injectiveproof · cited by 0