diff --git a/Mathlib/Algebra/Order/Ring/Cast.lean b/Mathlib/Algebra/Order/Ring/Cast.lean index 2f8d74e4b82bf..06e3f2297e000 100644 --- a/Mathlib/Algebra/Order/Ring/Cast.lean +++ b/Mathlib/Algebra/Order/Ring/Cast.lean @@ -24,15 +24,17 @@ open Function Nat variable {R : Type*} namespace Int -section OrderedRing -variable [OrderedRing R] +section OrderedAddCommGroupWithOne + +variable [AddCommGroupWithOne R] [PartialOrder R] [CovariantClass R R (· + ·) (· ≤ ·)] +variable [ZeroLEOneClass R] [NeZero (1 : R)] lemma cast_mono : Monotone (Int.cast : ℤ → R) := by intro m n h rw [← sub_nonneg] at h lift n - m to ℕ using h with k hk rw [← sub_nonneg, ← cast_sub, ← hk, cast_natCast] - exact k.cast_nonneg + exact k.cast_nonneg' variable [Nontrivial R] {m n : ℤ} @@ -56,7 +58,7 @@ lemma cast_strictMono : StrictMono (fun x : ℤ => (x : R)) := @[simp] lemma cast_lt_zero : (n : R) < 0 ↔ n < 0 := by rw [← cast_zero, cast_lt] -end OrderedRing +end OrderedAddCommGroupWithOne section LinearOrderedRing variable [LinearOrderedRing R] {a b n : ℤ} {x : R} diff --git a/Mathlib/Analysis/CstarAlgebra/Multiplier.lean b/Mathlib/Analysis/CstarAlgebra/Multiplier.lean index 292cdbe93975f..bc423401f3149 100644 --- a/Mathlib/Analysis/CstarAlgebra/Multiplier.lean +++ b/Mathlib/Analysis/CstarAlgebra/Multiplier.lean @@ -447,7 +447,7 @@ maps `Lₐ Rₐ : A →L[𝕜] A` given by left- and right-multiplication by `a` Warning: if `A = 𝕜`, then this is a coercion which is not definitionally equal to the `algebraMap 𝕜 𝓜(𝕜, 𝕜)` coercion, but these are propositionally equal. See `DoubleCentralizer.coe_eq_algebraMap` below. -/ --- Porting note: added `noncomputable` because an IR check failed? +-- Porting note: added `noncomputable`; IR check does not recognise `ContinuousLinearMap.mul` @[coe] protected noncomputable def coe (a : A) : 𝓜(𝕜, A) := { fst := ContinuousLinearMap.mul 𝕜 A a diff --git a/Mathlib/Analysis/Quaternion.lean b/Mathlib/Analysis/Quaternion.lean index 14a079dfa5a35..e41480ad1e545 100644 --- a/Mathlib/Analysis/Quaternion.lean +++ b/Mathlib/Analysis/Quaternion.lean @@ -86,7 +86,6 @@ noncomputable instance : NormedDivisionRing ℍ where simp only [norm_eq_sqrt_real_inner, inner_self, normSq.map_mul] exact Real.sqrt_mul normSq_nonneg _ --- Porting note: added `noncomputable` noncomputable instance : NormedAlgebra ℝ ℍ where norm_smul_le := norm_smul_le toAlgebra := Quaternion.algebra diff --git a/Mathlib/CategoryTheory/Monoidal/Types/Coyoneda.lean b/Mathlib/CategoryTheory/Monoidal/Types/Coyoneda.lean index ee138b0e38a78..633d6872c7ad0 100644 --- a/Mathlib/CategoryTheory/Monoidal/Types/Coyoneda.lean +++ b/Mathlib/CategoryTheory/Monoidal/Types/Coyoneda.lean @@ -25,14 +25,7 @@ open Opposite open MonoidalCategory --- Porting note: made it noncomputable. --- `failed to compile definition, consider marking it as 'noncomputable' because it` --- `depends on 'CategoryTheory.typesMonoidal', and it does not have executable code` --- I don't know if that is a problem, might need to change it back in the future, but --- if so it might be better to fix then instead of at the moment of porting. - /-- `(𝟙_ C ⟶ -)` is a lax monoidal functor to `Type`. -/ -noncomputable def coyonedaTensorUnit (C : Type u) [Category.{v} C] [MonoidalCategory C] : LaxMonoidalFunctor C (Type v) := .ofTensorHom (F := coyoneda.obj (op (𝟙_ C))) diff --git a/Mathlib/Computability/PartrecCode.lean b/Mathlib/Computability/PartrecCode.lean index 5bb50ca1e5675..d061b8f7736f9 100644 --- a/Mathlib/Computability/PartrecCode.lean +++ b/Mathlib/Computability/PartrecCode.lean @@ -79,7 +79,6 @@ inductive Code : Type | prec : Code → Code → Code | rfind' : Code → Code --- Porting note: `Nat.Partrec.Code.recOn` is noncomputable in Lean4, so we make it computable. compile_inductive% Code end Nat.Partrec diff --git a/Mathlib/Computability/TMToPartrec.lean b/Mathlib/Computability/TMToPartrec.lean index 762a216837a6e..dcc03fdf10e6c 100644 --- a/Mathlib/Computability/TMToPartrec.lean +++ b/Mathlib/Computability/TMToPartrec.lean @@ -867,7 +867,6 @@ inductive Λ' | pred (q₁ q₂ : Λ') | ret (k : Cont') --- Porting note: `Turing.PartrecToTM2.Λ'.rec` is noncomputable in Lean4, so we make it computable. compile_inductive% Code compile_inductive% Cont' compile_inductive% K' diff --git a/Mathlib/Data/Analysis/Topology.lean b/Mathlib/Data/Analysis/Topology.lean index 1e7c2003dc521..f8db5f20dd999 100644 --- a/Mathlib/Data/Analysis/Topology.lean +++ b/Mathlib/Data/Analysis/Topology.lean @@ -153,10 +153,8 @@ theorem ext [T : TopologicalSpace α] {σ : Type*} {F : Ctop α σ} (H₁ : ∀ variable [TopologicalSpace α] --- Porting note: add non-computable : because --- > ... it depends on `Inter.inter`, and it does not have executable code. /-- The topological space realizer made of the open sets. -/ -protected noncomputable def id : Realizer α := +protected def id : Realizer α := ⟨{ x : Set α // IsOpen x }, { f := Subtype.val top := fun _ ↦ ⟨univ, isOpen_univ⟩ diff --git a/Mathlib/MeasureTheory/Measure/Haar/Basic.lean b/Mathlib/MeasureTheory/Measure/Haar/Basic.lean index e0216810f736e..4710b819f0406 100644 --- a/Mathlib/MeasureTheory/Measure/Haar/Basic.lean +++ b/Mathlib/MeasureTheory/Measure/Haar/Basic.lean @@ -83,10 +83,6 @@ variable {G : Type*} [Group G] namespace haar --- Porting note: Even in `noncomputable section`, a definition with `to_additive` require --- `noncomputable` to generate an additive definition. --- Please refer to leanprover/lean4#2077. - /-- The index or Haar covering number or ratio of `K` w.r.t. `V`, denoted `(K : V)`: it is the smallest number of (left) translates of `V` that is necessary to cover `K`. It is defined to be 0 if no finite number of translates cover `K`. -/ @@ -341,11 +337,6 @@ theorem nonempty_iInter_clPrehaar (K₀ : PositiveCompacts G) : ### Lemmas about `chaar` -/ - --- Porting note: Even in `noncomputable section`, a definition with `to_additive` require --- `noncomputable` to generate an additive definition. --- Please refer to leanprover/lean4#2077. - /-- This is the "limit" of `prehaar K₀ U K` as `U` becomes a smaller and smaller open neighborhood of `(1 : G)`. More precisely, it is defined to be an arbitrary element in the intersection of all the sets `clPrehaar K₀ V` in `haarProduct K₀`. @@ -463,10 +454,6 @@ theorem is_left_invariant_chaar {K₀ : PositiveCompacts G} (g : G) (K : Compact apply is_left_invariant_prehaar; rw [h2U.interior_eq]; exact ⟨1, h3U⟩ · apply continuous_iff_isClosed.mp this; exact isClosed_singleton --- Porting note: Even in `noncomputable section`, a definition with `to_additive` require --- `noncomputable` to generate an additive definition. --- Please refer to leanprover/lean4#2077. - /-- The function `chaar` interpreted in `ℝ≥0`, as a content -/ @[to_additive "additive version of `MeasureTheory.Measure.haar.haarContent`"] noncomputable def haarContent (K₀ : PositiveCompacts G) : Content G where @@ -518,13 +505,8 @@ open haar ### The Haar measure -/ - variable [TopologicalSpace G] [TopologicalGroup G] [MeasurableSpace G] [BorelSpace G] --- Porting note: Even in `noncomputable section`, a definition with `to_additive` require --- `noncomputable` to generate an additive definition. --- Please refer to leanprover/lean4#2077. - /-- The Haar measure on the locally compact group `G`, scaled so that `haarMeasure K₀ K₀ = 1`. -/ @[to_additive "The Haar measure on the locally compact additive group `G`, scaled so that