diff --git a/Mathlib/Algebra/Field/Defs.lean b/Mathlib/Algebra/Field/Defs.lean index d07e14959ce750..cbbb7f6706e425 100644 --- a/Mathlib/Algebra/Field/Defs.lean +++ b/Mathlib/Algebra/Field/Defs.lean @@ -7,6 +7,7 @@ module public import Mathlib.Algebra.Ring.Defs public import Mathlib.Data.Rat.Init +public import Mathlib.Tactic.FastInstance /-! # Division (semi)rings and (semi)fields @@ -180,7 +181,8 @@ If the field has positive characteristic `p`, our division by zero convention fo class Field (K : Type u) extends CommRing K, DivisionRing K -- see Note [lower instance priority] -instance (priority := 100) Field.toSemifield [Field K] : Semifield K := { ‹Field K› with } +instance (priority := 100) Field.toSemifield [Field K] : Semifield K := + fast_instance% { ‹Field K› with } namespace NNRat variable [DivisionSemiring K] diff --git a/Mathlib/Algebra/Order/Floor/Ring.lean b/Mathlib/Algebra/Order/Floor/Ring.lean index eed64193bb04d5..9dfeb7e65018cd 100644 --- a/Mathlib/Algebra/Order/Floor/Ring.lean +++ b/Mathlib/Algebra/Order/Floor/Ring.lean @@ -586,7 +586,7 @@ theorem add_one_le_ceil_iff : z + 1 ≤ ⌈a⌉ ↔ (z : R) < a := by rw [← lt @[simp] theorem one_le_ceil_iff : 1 ≤ ⌈a⌉ ↔ 0 < a := by - simpa using le_ceil_iff (z := 1) + simpa using le_ceil_iff (R := R) (z := 1) @[bound] theorem ceil_le_floor_add_one (a : R) : ⌈a⌉ ≤ ⌊a⌋ + 1 := by diff --git a/Mathlib/Algebra/Ring/Defs.lean b/Mathlib/Algebra/Ring/Defs.lean index 81985b459da99c..3bd5469ed1a34d 100644 --- a/Mathlib/Algebra/Ring/Defs.lean +++ b/Mathlib/Algebra/Ring/Defs.lean @@ -9,6 +9,7 @@ public import Mathlib.Algebra.GroupWithZero.Defs public import Mathlib.Data.Int.Cast.Defs public import Mathlib.Tactic.Spread public import Mathlib.Tactic.StacksAttribute +public import Mathlib.Tactic.FastInstance /-! # Semirings and rings @@ -145,6 +146,16 @@ class Semiring (α : Type u) extends NonUnitalSemiring α, NonAssocSemiring α, /-- A `Ring` is a `Semiring` with negation making it an additive group. -/ class Ring (R : Type u) extends Semiring R, AddCommGroup R, AddGroupWithOne R +attribute [-instance] Ring.toAddGroupWithOne + +instance Ring.toAddGroupWithOne' (R : Type u) [Ring R] : AddGroupWithOne R := + @AddGroupWithOne.mk R Ring.toIntCast inferInstance inferInstance + inferInstance Ring.sub_eq_add_neg Ring.zsmul Ring.zsmul_zero' Ring.zsmul_succ' + Ring.zsmul_neg' Ring.neg_add_cancel intCast_ofNat intCast_negSucc + +instance Ring.toAddCommGroup' (R : Type u) [self : Ring R] : AddCommGroup R := + @AddCommGroup.mk R inferInstance add_comm' + /-! ### Semirings -/ @@ -369,12 +380,12 @@ variable [Ring α] -- A (unital, associative) ring is a not-necessarily-unital ring -- see Note [lower instance priority] instance (priority := 100) Ring.toNonUnitalRing : NonUnitalRing α := - { ‹Ring α› with } + fast_instance% { ‹Ring α› with } -- A (unital, associative) ring is a not-necessarily-associative ring -- see Note [lower instance priority] instance (priority := 100) Ring.toNonAssocRing : NonAssocRing α := - { ‹Ring α› with } + fast_instance% { ‹Ring α› with } end Ring @@ -386,6 +397,11 @@ class NonUnitalNonAssocCommRing (α : Type u) /-- A non-unital commutative ring is a `NonUnitalRing` with commutative multiplication. -/ class NonUnitalCommRing (α : Type u) extends NonUnitalRing α, NonUnitalNonAssocCommRing α +instance NonUnitalCommRing.toNonUnitalNonAssocCommRing' (α : Type u) + [self : NonUnitalCommRing α] : NonUnitalNonAssocCommRing α := + @NonUnitalNonAssocCommRing.mk α + self.toNonUnitalRing.toNonUnitalNonAssocRing NonUnitalCommRing.mul_comm + /-- A non-associative commutative ring is a `NonAssocRing` with commutative multiplication. -/ class NonAssocCommRing (α : Type u) extends NonAssocRing α, NonUnitalNonAssocCommRing α, NonAssocCommSemiring α @@ -409,12 +425,12 @@ instance (priority := 100) CommRing.toCommSemiring [s : CommRing α] : CommSemir -- see Note [lower instance priority] instance (priority := 100) CommRing.toNonUnitalCommRing [s : CommRing α] : NonUnitalCommRing α := - { s with } + fast_instance% { s with } -- see Note [lower instance priority] instance (priority := 100) CommRing.toAddCommGroupWithOne [s : CommRing α] : AddCommGroupWithOne α := - { s with } + fast_instance% { s with } /-- A domain is a nontrivial semiring such that multiplication by a nonzero element is cancellative on both sides. In other words, a nontrivial semiring `R` satisfying diff --git a/Mathlib/Analysis/CStarAlgebra/Matrix.lean b/Mathlib/Analysis/CStarAlgebra/Matrix.lean index 7d4a867e9e28da..a5658cc85dae51 100644 --- a/Mathlib/Analysis/CStarAlgebra/Matrix.lean +++ b/Mathlib/Analysis/CStarAlgebra/Matrix.lean @@ -243,7 +243,7 @@ lemma l2_opNorm_diagonal (v : n → 𝕜) : ‖(diagonal v : Matrix n n 𝕜)‖ calc _ = ‖T (toLp 2 (Pi.single i (1 : 𝕜)))‖ := by rw [toEuclideanCLM_toLp (diagonal v) (Pi.single i (1 : 𝕜))] simp - _ ≤ _ := by grw [T.le_opNorm]; simp + _ ≤ _ := by grw [T.le_opNorm]; simp [-CStarRing.norm_of_mem_unitary] -- simp perf boost @[simp] lemma l2_opNNNorm_diagonal (v : n → 𝕜) : ‖(diagonal v : Matrix n n 𝕜)‖₊ = ‖v‖₊ := diff --git a/Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean b/Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean index a79759b360c07c..94b1f87628cdeb 100644 --- a/Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean +++ b/Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean @@ -700,10 +700,11 @@ open IntermediateField universe u v + variable {K : Type u} [NontriviallyNormedField K] {L : Type v} [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] [hu : IsUltrametricDist K] -set_option backward.inferInstanceAs.wrap.data false in +set_option trace.Meta.synthInstance true in /-- If `K` is a field complete with respect to a nontrivial nonarchimedean multiplicative norm and `L/K` is an algebraic extension, then any power-multiplicative `K`-algebra norm on `L` coincides with the spectral norm. -/ @@ -711,9 +712,9 @@ theorem spectralNorm_unique [CompleteSpace K] {f : AlgebraNorm K L} (hf_pm : IsP f = spectralAlgNorm K L := by apply eq_of_powMul_faithful f hf_pm _ spectralAlgNorm_isPowMul intro x - set E : Type v := id K⟮x⟯ - letI hE : Field E := inferInstanceAs (Field K⟮x⟯) - letI : Algebra K E := inferInstanceAs (Algebra K K⟮x⟯) + let E : Type v := id K⟮x⟯ + let : Field E := show Field K⟮x⟯ by infer_instance + let : Module K E := show Module K K⟮x⟯ by infer_instance let id1 : K⟮x⟯ →ₗ[K] E := LinearMap.id let id2 : E →ₗ[K] K⟮x⟯ := LinearMap.id set hs_norm : RingNorm E := @@ -729,8 +730,9 @@ theorem spectralNorm_unique [CompleteSpace K] {f : AlgebraNorm K L} (hf_pm : IsP eq_zero_of_map_eq_zero' a ha := by simpa [id_eq, eq_mpr_eq_cast, cast_eq, LinearMap.coe_mk, ← spectralAlgNorm_def, map_eq_zero_iff_eq_zero, ZeroMemClass.coe_eq_zero] using ha } - letI n1 : NormedRing E := RingNorm.toNormedRing hs_norm - letI N1 : NormedSpace K E := + let n1 : NormedRing E := RingNorm.toNormedRing hs_norm + have : IsTopologicalAddGroup E := SeminormedAddCommGroup.toIsTopologicalAddGroup + let N1 : NormedSpace K E := { one_smul e := by simp [one_smul] mul_smul k1 k2 e := by simp [mul_smul] smul_zero e := by simp @@ -749,8 +751,8 @@ theorem spectralNorm_unique [CompleteSpace K] {f : AlgebraNorm K L} (hf_pm : IsP mul_le' a b := map_mul_le_mul _ _ _ eq_zero_of_map_eq_zero' a ha := by simpa [map_eq_zero_iff_eq_zero, map_eq_zero] using ha } - letI n2 : NormedRing K⟮x⟯ := RingNorm.toNormedRing hf_norm - letI N2 : NormedSpace K K⟮x⟯ := + let n2 : NormedRing K⟮x⟯ := RingNorm.toNormedRing hf_norm + let N2 : NormedSpace K K⟮x⟯ := { one_smul e := by simp [one_smul] mul_smul k1 k2 e := by simp [mul_smul] smul_zero e := by simp @@ -762,9 +764,9 @@ theorem spectralNorm_unique [CompleteSpace K] {f : AlgebraNorm K L} (hf_pm : IsP have : (algebraMap (↥K⟮x⟯) L) (k • y) = k • algebraMap (↥K⟮x⟯) L y := by simp [IntermediateField.algebraMap_apply] rw [this, map_smul_eq_mul] } - haveI hKx_fin : FiniteDimensional K ↥K⟮x⟯ := + have hKx_fin : FiniteDimensional K ↥K⟮x⟯ := IntermediateField.adjoin.finiteDimensional (Algebra.IsAlgebraic.isAlgebraic x).isIntegral - haveI : FiniteDimensional K E := hKx_fin + have : FiniteDimensional K E := hKx_fin set Id1 : K⟮x⟯ →L[K] E := ⟨id1, id1.continuous_of_finiteDimensional⟩ set Id2 : E →L[K] K⟮x⟯ := ⟨id2, id2.continuous_of_finiteDimensional⟩ obtain ⟨C1, hC1_pos, hC1⟩ : ∃ C1 : ℝ, 0 < C1 ∧ ∀ y : K⟮x⟯, ‖id1 y‖ ≤ C1 * ‖y‖ := diff --git a/Mathlib/Analysis/RCLike/Basic.lean b/Mathlib/Analysis/RCLike/Basic.lean index 6126e1b075c3a1..2bb4179782c539 100644 --- a/Mathlib/Analysis/RCLike/Basic.lean +++ b/Mathlib/Analysis/RCLike/Basic.lean @@ -787,7 +787,6 @@ lemma norm_expect_le {ι : Type*} {s : Finset ι} {f : ι → E} : ‖𝔼 i ∈ Finset.le_expect_of_subadditive norm_zero norm_add_le fun _ _ ↦ by rw [norm_nnqsmul K] end NormedField - section Order open scoped ComplexOrder diff --git a/Mathlib/Data/Int/Cast/Defs.lean b/Mathlib/Data/Int/Cast/Defs.lean index 281e7b622c16ce..348a699070aa42 100644 --- a/Mathlib/Data/Int/Cast/Defs.lean +++ b/Mathlib/Data/Int/Cast/Defs.lean @@ -46,6 +46,33 @@ class AddGroupWithOne (R : Type u) extends IntCast R, AddMonoidWithOne R, AddGro of the canonical homomorphism `ℕ → R`. -/ intCast_negSucc : ∀ n : ℕ, intCast (Int.negSucc n) = -Nat.cast (n + 1) := by intros; rfl +instance AddGroupWithOne.toSubNegMonoid {R : Type u} [self : AddGroupWithOne R] : + SubNegMonoid R := + (@SubNegMonoid.mk R self.toAddMonoid self.toNeg self.toSub + AddGroupWithOne.sub_eq_add_neg self.zsmul AddGroupWithOne.zsmul_zero' + AddGroupWithOne.zsmul_succ' AddGroupWithOne.zsmul_neg') + +attribute [-instance] AddGroupWithOne.toAddGroup in +@[reducible] instance AddGroupWithOne.toAddGroup' {R : Type u} + [self : AddGroupWithOne R] : AddGroup R := + @AddGroup.mk R self.toSubNegMonoid AddGroupWithOne.neg_add_cancel + +-- section synth + +-- attribute [-instance] AddGroupWithOne.toAddMonoidWithOne +-- variable (R : Type u) [self : AddGroupWithOne R] +-- #synth NatCast R +-- #synth AddMonoid R +-- #synth One R + +-- end synth + +--attribute [-instance] AddGroupWithOne.toAddMonoidWithOne in +instance AddGroupWithOne.toAddMonoidWithOne' (R : Type u) [self : AddGroupWithOne R] : + AddMonoidWithOne R := + @AddMonoidWithOne.mk R _ self.toAddGroup'.toAddMonoid _ + AddMonoidWithOne.natCast_zero Nat.cast_succ + /-- An `AddCommGroupWithOne` is an `AddGroupWithOne` satisfying `a + b = b + a`. -/ class AddCommGroupWithOne (R : Type u) extends AddCommGroup R, AddGroupWithOne R, AddCommMonoidWithOne R