Skip to content

Commit

Permalink
chore: solve not necessary anymore porting notes (#11086)
Browse files Browse the repository at this point in the history
Solves porting notes claiming
- "not necessary anymore" 
- "not used anymore"

by simply deleting them.
  • Loading branch information
pitmonticone committed Mar 1, 2024
1 parent 8f422f3 commit 86b7828
Show file tree
Hide file tree
Showing 4 changed files with 1 addition and 14 deletions.
2 changes: 1 addition & 1 deletion Mathlib/Data/SetLike/Basic.lean
Expand Up @@ -187,7 +187,7 @@ theorem coe_eq_coe {x y : p} : (x : B) = y ↔ x = y :=
#align set_like.coe_eq_coe SetLike.coe_eq_coe

-- porting note: this is not necessary anymore due to the way coercions work
#noalign set_like.coe_mk
#noalign set_like.coe_mk

@[simp]
theorem coe_mem (x : p) : (x : B) ∈ p :=
Expand Down
3 changes: 0 additions & 3 deletions Mathlib/LinearAlgebra/GeneralLinearGroup.lean
Expand Up @@ -37,9 +37,6 @@ namespace GeneralLinearGroup

variable {R M}

-- Porting note: This is not necessary anymore
-- instance : CoeFun (GeneralLinearGroup R M) fun _ ↦ M → M := by infer_instance

/-- An invertible linear map `f` determines an equivalence from `M` to itself. -/
def toLinearEquiv (f : GeneralLinearGroup R M) : M ≃ₗ[R] M :=
{ f.val with
Expand Down
5 changes: 0 additions & 5 deletions Mathlib/NumberTheory/Dioph.lean
Expand Up @@ -102,11 +102,6 @@ instance instFunLike : FunLike (Poly α) (α → ℕ) ℤ :=
⟨Subtype.val, Subtype.val_injective⟩
#align poly.fun_like Poly.instFunLike

-- Porting note: This instance is not necessary anymore
-- /-- Helper instance for when there are too many metavariables to apply `DFunLike.hasCoeToFun`
-- directly. -/
-- instance : CoeFun (Poly α) fun _ => (α → ℕ) → ℤ := DFunLike.hasCoeToFun

/-- The underlying function of a `Poly` is a polynomial -/
protected theorem isPoly (f : Poly α) : IsPoly f := f.2
#align poly.is_poly Poly.isPoly
Expand Down
5 changes: 0 additions & 5 deletions Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
Expand Up @@ -158,11 +158,6 @@ def UniformOnFun (α β : Type*) (_ : Set (Set α)) :=

@[inherit_doc] scoped[UniformConvergence] notation:25 α " →ᵤ[" 𝔖 "] " β:0 => UniformOnFun α β 𝔖

-- Porting note: these are not used anymore
-- scoped[UniformConvergence] notation3 "λᵘ "(...)", "r:(scoped p => UniformFun.ofFun p) => r

-- scoped[UniformConvergence] notation3 "λᵘ["𝔖"] "(...)", "r:(scoped p => UniformFun.ofFun p) => r

open UniformConvergence

variable {α β : Type*} {𝔖 : Set (Set α)}
Expand Down

0 comments on commit 86b7828

Please sign in to comment.