Skip to content

Commit

Permalink
chore: Delete some orphaned porting notes (#10230)
Browse files Browse the repository at this point in the history
Delete some porting notes that are now orphaned.
  • Loading branch information
mattrobball authored and apnelson1 committed May 12, 2024
1 parent ddbd7d5 commit 96b025b
Showing 1 changed file with 0 additions and 3 deletions.
3 changes: 0 additions & 3 deletions Mathlib/FieldTheory/RatFunc.lean
Original file line number Diff line number Diff line change
Expand Up @@ -884,7 +884,6 @@ theorem liftMonoidWithZeroHom_apply_div {L : Type*} [CommGroupWithZero L]
liftMonoidWithZeroHom_apply_ofFractionRing_mk]
#align ratfunc.lift_monoid_with_zero_hom_apply_div RatFunc.liftMonoidWithZeroHom_apply_div

-- Porting note: added `simpNF` form of `liftMonoidWithZeroHom_apply_div`
@[simp]
theorem liftMonoidWithZeroHom_apply_div' {L : Type*} [CommGroupWithZero L]
(φ : MonoidWithZeroHom K[X] L) (hφ : K[X]⁰ ≤ L⁰.comap φ) (p q : K[X]) :
Expand All @@ -897,7 +896,6 @@ theorem liftRingHom_apply_div {L : Type*} [Field L] (φ : K[X] →+* L) (hφ : K
liftMonoidWithZeroHom_apply_div _ hφ _ _ -- Porting note: gave explicitly the `hφ`
#align ratfunc.lift_ring_hom_apply_div RatFunc.liftRingHom_apply_div

-- Porting note: added `simpNF` form of `liftRingHom_apply_div`
@[simp]
theorem liftRingHom_apply_div' {L : Type*} [Field L] (φ : K[X] →+* L) (hφ : K[X]⁰ ≤ L⁰.comap φ)
(p q : K[X]) : liftRingHom φ hφ (algebraMap _ _ p) / liftRingHom φ hφ (algebraMap _ _ q) =
Expand Down Expand Up @@ -969,7 +967,6 @@ theorem liftAlgHom_injective (φ : K[X] →ₐ[S] L) (hφ : Function.Injective
liftMonoidWithZeroHom_injective _ hφ
#align ratfunc.lift_alg_hom_injective RatFunc.liftAlgHom_injective

-- Porting note: added `simpNF` form of `liftAlgHom_apply_div`
@[simp]
theorem liftAlgHom_apply_div' (p q : K[X]) :
liftAlgHom φ hφ (algebraMap _ _ p) / liftAlgHom φ hφ (algebraMap _ _ q) = φ p / φ q :=
Expand Down

0 comments on commit 96b025b

Please sign in to comment.