diff --git a/Mathbin/Algebra/Algebra/Spectrum.lean b/Mathbin/Algebra/Algebra/Spectrum.lean index f4770cceb9..34f1e85525 100644 --- a/Mathbin/Algebra/Algebra/Spectrum.lean +++ b/Mathbin/Algebra/Algebra/Spectrum.lean @@ -57,6 +57,7 @@ variable [CommSemiring R] [Ring A] [Algebra R A] -- mathport name: «expr↑ₐ» local notation "↑ₐ" => algebraMap R A +#print resolventSet /- -- definition and basic properties /-- Given a commutative ring `R` and an `R`-algebra `A`, the *resolvent set* of `a : A` is the `set R` consisting of those `r : R` for which `r•1 - a` is a unit of the @@ -64,7 +65,9 @@ algebra `A`. -/ def resolventSet (a : A) : Set R := {r : R | IsUnit (↑ₐ r - a)} #align resolvent_set resolventSet +-/ +#print spectrum /- /-- Given a commutative ring `R` and an `R`-algebra `A`, the *spectrum* of `a : A` is the `set R` consisting of those `r : R` for which `r•1 - a` is not a unit of the algebra `A`. @@ -73,25 +76,28 @@ The spectrum is simply the complement of the resolvent set. -/ def spectrum (a : A) : Set R := resolventSet R aᶜ #align spectrum spectrum +-/ variable {R} +#print resolvent /- /-- Given an `a : A` where `A` is an `R`-algebra, the *resolvent* is a map `R → A` which sends `r : R` to `(algebra_map R A r - a)⁻¹` when `r ∈ resolvent R A` and `0` when `r ∈ spectrum R A`. -/ noncomputable def resolvent (a : A) (r : R) : A := Ring.inverse (↑ₐ r - a) #align resolvent resolvent +-/ /-- The unit `1 - r⁻¹ • a` constructed from `r • 1 - a` when the latter is a unit. -/ @[simps] -noncomputable def IsUnit.subInvSmul {r : Rˣ} {s : R} {a : A} (h : IsUnit <| r • ↑ₐ s - a) : Aˣ +noncomputable def IsUnit.subInvSMul {r : Rˣ} {s : R} {a : A} (h : IsUnit <| r • ↑ₐ s - a) : Aˣ where val := ↑ₐ s - r⁻¹ • a inv := r • ↑h.Unit⁻¹ val_inv := by rw [mul_smul_comm, ← smul_mul_assoc, smul_sub, smul_inv_smul, h.mul_coe_inv] inv_val := by rw [smul_mul_assoc, ← mul_smul_comm, smul_sub, smul_inv_smul, h.coe_inv_mul] -#align is_unit.sub_inv_smul IsUnit.subInvSmul +#align is_unit.sub_inv_smul IsUnit.subInvSMul end Defs @@ -138,15 +144,19 @@ theorem mem_resolventSet_iff {r : R} {a : A} : r ∈ resolventSet R a ↔ IsUnit Iff.rfl #align spectrum.mem_resolvent_set_iff spectrum.mem_resolventSet_iff +#print spectrum.resolventSet_of_subsingleton /- @[simp] theorem resolventSet_of_subsingleton [Subsingleton A] (a : A) : resolventSet R a = Set.univ := by simp_rw [resolventSet, Subsingleton.elim (algebraMap R A _ - a) 1, isUnit_one, Set.setOf_true] #align spectrum.resolvent_set_of_subsingleton spectrum.resolventSet_of_subsingleton +-/ +#print spectrum.of_subsingleton /- @[simp] theorem of_subsingleton [Subsingleton A] (a : A) : spectrum R a = ∅ := by rw [spectrum, resolvent_set_of_subsingleton, Set.compl_univ] #align spectrum.of_subsingleton spectrum.of_subsingleton +-/ theorem resolvent_eq {a : A} {r : R} (h : r ∈ resolventSet R a) : resolvent a r = ↑h.Unit⁻¹ := Ring.inverse_unit h.Unit @@ -170,11 +180,13 @@ theorem units_smul_resolvent {r : Rˣ} {s : R} {a : A} : simp only [Algebra.algebraMap_eq_smul_one, smul_assoc, smul_inv_smul] #align spectrum.units_smul_resolvent spectrum.units_smul_resolvent +#print spectrum.units_smul_resolvent_self /- theorem units_smul_resolvent_self {r : Rˣ} {a : A} : r • resolvent a (r : R) = resolvent (r⁻¹ • a) (1 : R) := by simpa only [Units.smul_def, Algebra.id.smul_eq_mul, Units.inv_mul] using @units_smul_resolvent _ _ _ _ _ r r a #align spectrum.units_smul_resolvent_self spectrum.units_smul_resolvent_self +-/ /-- The resolvent is a unit when the argument is in the resolvent set. -/ theorem isUnit_resolvent {r : R} {a : A} : r ∈ resolventSet R a ↔ IsUnit (resolvent a r) := @@ -262,16 +274,20 @@ section Star variable [InvolutiveStar R] [StarRing A] [StarModule R A] +#print spectrum.star_mem_resolventSet_iff /- theorem star_mem_resolventSet_iff {r : R} {a : A} : star r ∈ resolventSet R a ↔ r ∈ resolventSet R (star a) := by refine' ⟨fun h => _, fun h => _⟩ <;> simpa only [mem_resolvent_set_iff, Algebra.algebraMap_eq_smul_one, star_sub, star_smul, star_star, star_one] using IsUnit.star h #align spectrum.star_mem_resolvent_set_iff spectrum.star_mem_resolventSet_iff +-/ +#print spectrum.map_star /- protected theorem map_star (a : A) : σ (star a) = star (σ a) := by ext; simpa only [Set.mem_star, mem_iff, not_iff_not] using star_mem_resolvent_set_iff.symm #align spectrum.map_star spectrum.map_star +-/ end Star @@ -294,11 +310,13 @@ theorem subset_subalgebra {S : Subalgebra R A} (a : S) : spectrum R (a : A) ⊆ compl_subset_compl.2 fun _ => IsUnit.map S.val #align spectrum.subset_subalgebra spectrum.subset_subalgebra +#print spectrum.subset_starSubalgebra /- -- this is why it would be nice if `subset_subalgebra` was registered for `subalgebra_class`. theorem subset_starSubalgebra [StarRing R] [StarRing A] [StarModule R A] {S : StarSubalgebra R A} (a : S) : spectrum R (a : A) ⊆ spectrum R a := compl_subset_compl.2 fun _ => IsUnit.map S.Subtype #align spectrum.subset_star_subalgebra spectrum.subset_starSubalgebra +-/ theorem singleton_add_eq (a : A) (r : R) : {r} + σ a = σ (↑ₐ r + a) := ext fun x => by diff --git a/Mathbin/Algebra/Category/Module/Algebra.lean b/Mathbin/Algebra/Category/Module/Algebra.lean index 878e3521c4..49b60dc7f4 100644 --- a/Mathbin/Algebra/Category/Module/Algebra.lean +++ b/Mathbin/Algebra/Category/Module/Algebra.lean @@ -45,17 +45,21 @@ variable {k : Type u} [Field k] variable {A : Type w} [Ring A] [Algebra k A] +#print ModuleCat.moduleOfAlgebraModule /- /-- Type synonym for considering a module over a `k`-algebra as a `k`-module. -/ def moduleOfAlgebraModule (M : ModuleCat.{v} A) : Module k M := RestrictScalars.module k A M #align Module.module_of_algebra_Module ModuleCat.moduleOfAlgebraModule +-/ attribute [scoped instance] ModuleCat.moduleOfAlgebraModule +#print ModuleCat.isScalarTower_of_algebra_moduleCat /- theorem isScalarTower_of_algebra_moduleCat (M : ModuleCat.{v} A) : IsScalarTower k A M := RestrictScalars.isScalarTower k A M #align Module.is_scalar_tower_of_algebra_Module ModuleCat.isScalarTower_of_algebra_moduleCat +-/ attribute [scoped instance] ModuleCat.isScalarTower_of_algebra_moduleCat diff --git a/Mathbin/Algebra/Lie/Classical.lean b/Mathbin/Algebra/Lie/Classical.lean index cd8919a350..2dfe93089c 100644 --- a/Mathbin/Algebra/Lie/Classical.lean +++ b/Mathbin/Algebra/Lie/Classical.lean @@ -110,16 +110,18 @@ section ElementaryBasis variable {n} [Fintype n] (i j : n) +#print LieAlgebra.SpecialLinear.Eb /- /-- When j ≠ i, the elementary matrices are elements of sl n R, in fact they are part of a natural basis of sl n R. -/ -def eb (h : j ≠ i) : sl n R := +def Eb (h : j ≠ i) : sl n R := ⟨Matrix.stdBasisMatrix i j (1 : R), show Matrix.stdBasisMatrix i j (1 : R) ∈ LinearMap.ker (Matrix.traceLinearMap n R R) from Matrix.StdBasisMatrix.trace_zero i j (1 : R) h⟩ -#align lie_algebra.special_linear.Eb LieAlgebra.SpecialLinear.eb +#align lie_algebra.special_linear.Eb LieAlgebra.SpecialLinear.Eb +-/ @[simp] -theorem eb_val (h : j ≠ i) : (eb R i j h).val = Matrix.stdBasisMatrix i j 1 := +theorem eb_val (h : j ≠ i) : (Eb R i j h).val = Matrix.stdBasisMatrix i j 1 := rfl #align lie_algebra.special_linear.Eb_val LieAlgebra.SpecialLinear.eb_val @@ -163,10 +165,12 @@ theorem mem_so [Fintype n] (A : Matrix n n R) : A ∈ so n R ↔ Aᵀ = -A := simp only [Matrix.IsSkewAdjoint, Matrix.IsAdjointPair, Matrix.mul_one, Matrix.one_mul] #align lie_algebra.orthogonal.mem_so LieAlgebra.Orthogonal.mem_so +#print LieAlgebra.Orthogonal.indefiniteDiagonal /- /-- The indefinite diagonal matrix with `p` 1s and `q` -1s. -/ def indefiniteDiagonal : Matrix (Sum p q) (Sum p q) R := Matrix.diagonal <| Sum.elim (fun _ => 1) fun _ => -1 #align lie_algebra.orthogonal.indefinite_diagonal LieAlgebra.Orthogonal.indefiniteDiagonal +-/ /-- The indefinite orthogonal Lie subalgebra: skew-adjoint matrices with respect to the symmetric bilinear form defined by the indefinite diagonal matrix. -/ @@ -174,15 +178,17 @@ def so' [Fintype p] [Fintype q] : LieSubalgebra R (Matrix (Sum p q) (Sum p q) R) skewAdjointMatricesLieSubalgebra <| indefiniteDiagonal p q R #align lie_algebra.orthogonal.so' LieAlgebra.Orthogonal.so' +#print LieAlgebra.Orthogonal.Pso /- /-- A matrix for transforming the indefinite diagonal bilinear form into the definite one, provided the parameter `i` is a square root of -1. -/ -def pso (i : R) : Matrix (Sum p q) (Sum p q) R := +def Pso (i : R) : Matrix (Sum p q) (Sum p q) R := Matrix.diagonal <| Sum.elim (fun _ => 1) fun _ => i -#align lie_algebra.orthogonal.Pso LieAlgebra.Orthogonal.pso +#align lie_algebra.orthogonal.Pso LieAlgebra.Orthogonal.Pso +-/ variable [Fintype p] [Fintype q] -theorem pso_inv {i : R} (hi : i * i = -1) : pso p q R i * pso p q R (-i) = 1 := +theorem pso_inv {i : R} (hi : i * i = -1) : Pso p q R i * Pso p q R (-i) = 1 := by ext (x y); rcases x with ⟨⟩ <;> rcases y with ⟨⟩ ·-- x y : p @@ -198,12 +204,12 @@ theorem pso_inv {i : R} (hi : i * i = -1) : pso p q R i * pso p q R (-i) = 1 := #align lie_algebra.orthogonal.Pso_inv LieAlgebra.Orthogonal.pso_inv /-- There is a constructive inverse of `Pso p q R i`. -/ -def invertiblePso {i : R} (hi : i * i = -1) : Invertible (pso p q R i) := +def invertiblePso {i : R} (hi : i * i = -1) : Invertible (Pso p q R i) := invertibleOfRightInverse _ _ (pso_inv p q R hi) #align lie_algebra.orthogonal.invertible_Pso LieAlgebra.Orthogonal.invertiblePso theorem indefiniteDiagonal_transform {i : R} (hi : i * i = -1) : - (pso p q R i)ᵀ ⬝ indefiniteDiagonal p q R ⬝ pso p q R i = 1 := + (Pso p q R i)ᵀ ⬝ indefiniteDiagonal p q R ⬝ Pso p q R i = 1 := by ext (x y); rcases x with ⟨⟩ <;> rcases y with ⟨⟩ ·-- x y : p @@ -231,10 +237,11 @@ def soIndefiniteEquiv {i : R} (hi : i * i = -1) : so' p q R ≃ₗ⁅R⁆ so (Su theorem soIndefiniteEquiv_apply {i : R} (hi : i * i = -1) (A : so' p q R) : (soIndefiniteEquiv p q R hi A : Matrix (Sum p q) (Sum p q) R) = - (pso p q R i)⁻¹ ⬝ (A : Matrix (Sum p q) (Sum p q) R) ⬝ pso p q R i := + (Pso p q R i)⁻¹ ⬝ (A : Matrix (Sum p q) (Sum p q) R) ⬝ Pso p q R i := by erw [LieEquiv.trans_apply, LieEquiv.ofEq_apply, skewAdjointMatricesLieSubalgebraEquiv_apply] #align lie_algebra.orthogonal.so_indefinite_equiv_apply LieAlgebra.Orthogonal.soIndefiniteEquiv_apply +#print LieAlgebra.Orthogonal.JD /- /-- A matrix defining a canonical even-rank symmetric bilinear form. It looks like this as a `2l x 2l` matrix of `l x l` blocks: @@ -242,16 +249,18 @@ It looks like this as a `2l x 2l` matrix of `l x l` blocks: [ 0 1 ] [ 1 0 ] -/ -def jD : Matrix (Sum l l) (Sum l l) R := +def JD : Matrix (Sum l l) (Sum l l) R := Matrix.fromBlocks 0 1 1 0 -#align lie_algebra.orthogonal.JD LieAlgebra.Orthogonal.jD +#align lie_algebra.orthogonal.JD LieAlgebra.Orthogonal.JD +-/ /-- The classical Lie algebra of type D as a Lie subalgebra of matrices associated to the matrix `JD`. -/ def typeD [Fintype l] := - skewAdjointMatricesLieSubalgebra (jD l R) + skewAdjointMatricesLieSubalgebra (JD l R) #align lie_algebra.orthogonal.type_D LieAlgebra.Orthogonal.typeD +#print LieAlgebra.Orthogonal.PD /- /-- A matrix transforming the bilinear form defined by the matrix `JD` into a split-signature diagonal matrix. @@ -260,40 +269,43 @@ It looks like this as a `2l x 2l` matrix of `l x l` blocks: [ 1 -1 ] [ 1 1 ] -/ -def pD : Matrix (Sum l l) (Sum l l) R := +def PD : Matrix (Sum l l) (Sum l l) R := Matrix.fromBlocks 1 (-1) 1 1 -#align lie_algebra.orthogonal.PD LieAlgebra.Orthogonal.pD +#align lie_algebra.orthogonal.PD LieAlgebra.Orthogonal.PD +-/ +#print LieAlgebra.Orthogonal.S /- /-- The split-signature diagonal matrix. -/ -def s := +def S := indefiniteDiagonal l l R -#align lie_algebra.orthogonal.S LieAlgebra.Orthogonal.s +#align lie_algebra.orthogonal.S LieAlgebra.Orthogonal.S +-/ -theorem s_as_blocks : s l R = Matrix.fromBlocks 1 0 0 (-1) := +theorem s_as_blocks : S l R = Matrix.fromBlocks 1 0 0 (-1) := by rw [← Matrix.diagonal_one, Matrix.diagonal_neg, Matrix.fromBlocks_diagonal] rfl #align lie_algebra.orthogonal.S_as_blocks LieAlgebra.Orthogonal.s_as_blocks -theorem jD_transform [Fintype l] : (pD l R)ᵀ ⬝ jD l R ⬝ pD l R = (2 : R) • s l R := +theorem jd_transform [Fintype l] : (PD l R)ᵀ ⬝ JD l R ⬝ PD l R = (2 : R) • S l R := by have h : (PD l R)ᵀ ⬝ JD l R = Matrix.fromBlocks 1 1 1 (-1) := by simp [PD, JD, Matrix.fromBlocks_transpose, Matrix.fromBlocks_multiply] erw [h, S_as_blocks, Matrix.fromBlocks_multiply, Matrix.fromBlocks_smul] congr <;> simp [two_smul] -#align lie_algebra.orthogonal.JD_transform LieAlgebra.Orthogonal.jD_transform +#align lie_algebra.orthogonal.JD_transform LieAlgebra.Orthogonal.jd_transform -theorem pD_inv [Fintype l] [Invertible (2 : R)] : pD l R * ⅟ (2 : R) • (pD l R)ᵀ = 1 := +theorem pd_inv [Fintype l] [Invertible (2 : R)] : PD l R * ⅟ (2 : R) • (PD l R)ᵀ = 1 := by have h : ⅟ (2 : R) • (1 : Matrix l l R) + ⅟ (2 : R) • 1 = 1 := by rw [← smul_add, ← two_smul R _, smul_smul, invOf_mul_self, one_smul] erw [Matrix.fromBlocks_transpose, Matrix.fromBlocks_smul, Matrix.mul_eq_mul, Matrix.fromBlocks_multiply] simp [h] -#align lie_algebra.orthogonal.PD_inv LieAlgebra.Orthogonal.pD_inv +#align lie_algebra.orthogonal.PD_inv LieAlgebra.Orthogonal.pd_inv -instance invertiblePD [Fintype l] [Invertible (2 : R)] : Invertible (pD l R) := - invertibleOfRightInverse _ _ (pD_inv l R) +instance invertiblePD [Fintype l] [Invertible (2 : R)] : Invertible (PD l R) := + invertibleOfRightInverse _ _ (pd_inv l R) #align lie_algebra.orthogonal.invertible_PD LieAlgebra.Orthogonal.invertiblePD /-- An equivalence between two possible definitions of the classical Lie algebra of type D. -/ @@ -302,11 +314,12 @@ def typeDEquivSo' [Fintype l] [Invertible (2 : R)] : typeD l R ≃ₗ⁅R⁆ so' apply (skewAdjointMatricesLieSubalgebraEquiv (JD l R) (PD l R) (by infer_instance)).trans apply LieEquiv.ofEq ext A - rw [JD_transform, ← coe_unitOfInvertible (2 : R), ← Units.smul_def, LieSubalgebra.mem_coe, + rw [JD_transform, ← unitOfInvertible_val (2 : R), ← Units.smul_def, LieSubalgebra.mem_coe, mem_skewAdjointMatricesLieSubalgebra_unit_smul] rfl #align lie_algebra.orthogonal.type_D_equiv_so' LieAlgebra.Orthogonal.typeDEquivSo' +#print LieAlgebra.Orthogonal.JB /- /-- A matrix defining a canonical odd-rank symmetric bilinear form. It looks like this as a `(2l+1) x (2l+1)` matrix of blocks: @@ -321,16 +334,18 @@ where sizes of the blocks are: [`l x 1` `l x l` `l x l`] [`l x 1` `l x l` `l x l`] -/ -def jB := - Matrix.fromBlocks ((2 : R) • 1 : Matrix Unit Unit R) 0 0 (jD l R) -#align lie_algebra.orthogonal.JB LieAlgebra.Orthogonal.jB +def JB := + Matrix.fromBlocks ((2 : R) • 1 : Matrix Unit Unit R) 0 0 (JD l R) +#align lie_algebra.orthogonal.JB LieAlgebra.Orthogonal.JB +-/ /-- The classical Lie algebra of type B as a Lie subalgebra of matrices associated to the matrix `JB`. -/ def typeB [Fintype l] := - skewAdjointMatricesLieSubalgebra (jB l R) + skewAdjointMatricesLieSubalgebra (JB l R) #align lie_algebra.orthogonal.type_B LieAlgebra.Orthogonal.typeB +#print LieAlgebra.Orthogonal.PB /- /-- A matrix transforming the bilinear form defined by the matrix `JB` into an almost-split-signature diagonal matrix. @@ -346,27 +361,28 @@ where sizes of the blocks are: [`l x 1` `l x l` `l x l`] [`l x 1` `l x l` `l x l`] -/ -def pB := - Matrix.fromBlocks (1 : Matrix Unit Unit R) 0 0 (pD l R) -#align lie_algebra.orthogonal.PB LieAlgebra.Orthogonal.pB +def PB := + Matrix.fromBlocks (1 : Matrix Unit Unit R) 0 0 (PD l R) +#align lie_algebra.orthogonal.PB LieAlgebra.Orthogonal.PB +-/ variable [Fintype l] -theorem pB_inv [Invertible (2 : R)] : pB l R * Matrix.fromBlocks 1 0 0 (⅟ (pD l R)) = 1 := +theorem pb_inv [Invertible (2 : R)] : PB l R * Matrix.fromBlocks 1 0 0 (⅟ (PD l R)) = 1 := by rw [PB, Matrix.mul_eq_mul, Matrix.fromBlocks_multiply, Matrix.mul_invOf_self] simp only [Matrix.mul_zero, Matrix.mul_one, Matrix.zero_mul, zero_add, add_zero, Matrix.fromBlocks_one] -#align lie_algebra.orthogonal.PB_inv LieAlgebra.Orthogonal.pB_inv +#align lie_algebra.orthogonal.PB_inv LieAlgebra.Orthogonal.pb_inv -instance invertiblePB [Invertible (2 : R)] : Invertible (pB l R) := - invertibleOfRightInverse _ _ (pB_inv l R) +instance invertiblePB [Invertible (2 : R)] : Invertible (PB l R) := + invertibleOfRightInverse _ _ (pb_inv l R) #align lie_algebra.orthogonal.invertible_PB LieAlgebra.Orthogonal.invertiblePB -theorem jB_transform : (pB l R)ᵀ ⬝ jB l R ⬝ pB l R = (2 : R) • Matrix.fromBlocks 1 0 0 (s l R) := by +theorem jb_transform : (PB l R)ᵀ ⬝ JB l R ⬝ PB l R = (2 : R) • Matrix.fromBlocks 1 0 0 (S l R) := by simp [PB, JB, JD_transform, Matrix.fromBlocks_transpose, Matrix.fromBlocks_multiply, Matrix.fromBlocks_smul] -#align lie_algebra.orthogonal.JB_transform LieAlgebra.Orthogonal.jB_transform +#align lie_algebra.orthogonal.JB_transform LieAlgebra.Orthogonal.jb_transform theorem indefiniteDiagonal_assoc : indefiniteDiagonal (Sum Unit l) l R = @@ -394,7 +410,7 @@ def typeBEquivSo' [Invertible (2 : R)] : typeB l R ≃ₗ⁅R⁆ so' (Sum Unit l (Matrix.reindexAlgEquiv _ (Equiv.sumAssoc PUnit l l)) (Matrix.transpose_reindex _ _)).trans apply LieEquiv.ofEq ext A - rw [JB_transform, ← coe_unitOfInvertible (2 : R), ← Units.smul_def, LieSubalgebra.mem_coe, + rw [JB_transform, ← unitOfInvertible_val (2 : R), ← Units.smul_def, LieSubalgebra.mem_coe, LieSubalgebra.mem_coe, mem_skewAdjointMatricesLieSubalgebra_unit_smul] simpa [indefinite_diagonal_assoc] #align lie_algebra.orthogonal.type_B_equiv_so' LieAlgebra.Orthogonal.typeBEquivSo' diff --git a/Mathbin/Algebra/Lie/TensorProduct.lean b/Mathbin/Algebra/Lie/TensorProduct.lean index e32719a150..bf53c35c0d 100644 --- a/Mathbin/Algebra/Lie/TensorProduct.lean +++ b/Mathbin/Algebra/Lie/TensorProduct.lean @@ -115,12 +115,10 @@ def lift : (M →ₗ[R] N →ₗ[R] P) ≃ₗ⁅R,L⁆ M ⊗[R] N →ₗ[R] P := #align tensor_product.lie_module.lift TensorProduct.LieModule.lift -/ -#print TensorProduct.LieModule.lift_apply /- @[simp] theorem lift_apply (f : M →ₗ[R] N →ₗ[R] P) (m : M) (n : N) : lift R L M N P f (m ⊗ₜ n) = f m n := rfl #align tensor_product.lie_module.lift_apply TensorProduct.LieModule.lift_apply --/ #print TensorProduct.LieModule.liftLie /- /-- A weaker form of the universal property for tensor product of modules of a Lie algebra. diff --git a/Mathbin/Algebra/Order/Interval.lean b/Mathbin/Algebra/Order/Interval.lean index 6aadce66fe..657cf1e681 100644 --- a/Mathbin/Algebra/Order/Interval.lean +++ b/Mathbin/Algebra/Order/Interval.lean @@ -51,45 +51,57 @@ instance : One (Interval α) := namespace NonemptyInterval +#print NonemptyInterval.toProd_one /- @[simp, to_additive to_prod_zero] theorem toProd_one : (1 : NonemptyInterval α).toProd = 1 := rfl #align nonempty_interval.to_prod_one NonemptyInterval.toProd_one #align nonempty_interval.to_prod_zero NonemptyInterval.toProd_zero +-/ +#print NonemptyInterval.fst_one /- @[to_additive] theorem fst_one : (1 : NonemptyInterval α).fst = 1 := rfl #align nonempty_interval.fst_one NonemptyInterval.fst_one #align nonempty_interval.fst_zero NonemptyInterval.fst_zero +-/ +#print NonemptyInterval.snd_one /- @[to_additive] theorem snd_one : (1 : NonemptyInterval α).snd = 1 := rfl #align nonempty_interval.snd_one NonemptyInterval.snd_one #align nonempty_interval.snd_zero NonemptyInterval.snd_zero +-/ +#print NonemptyInterval.coe_one_interval /- @[simp, norm_cast, to_additive] theorem coe_one_interval : ((1 : NonemptyInterval α) : Interval α) = 1 := rfl #align nonempty_interval.coe_one_interval NonemptyInterval.coe_one_interval #align nonempty_interval.coe_zero_interval NonemptyInterval.coe_zero_interval +-/ +#print NonemptyInterval.pure_one /- @[simp, to_additive] theorem pure_one : pure (1 : α) = 1 := rfl #align nonempty_interval.pure_one NonemptyInterval.pure_one #align nonempty_interval.pure_zero NonemptyInterval.pure_zero +-/ end NonemptyInterval namespace Interval +#print Interval.pure_one /- @[simp, to_additive] theorem pure_one : pure (1 : α) = 1 := rfl #align interval.pure_one Interval.pure_one #align interval.pure_zero Interval.pure_zero +-/ @[simp, to_additive] theorem one_ne_bot : (1 : Interval α) ≠ ⊥ := @@ -113,33 +125,41 @@ variable [PartialOrder α] [One α] namespace NonemptyInterval +#print NonemptyInterval.coe_one /- @[simp, to_additive] theorem coe_one : ((1 : NonemptyInterval α) : Set α) = 1 := coe_pure _ #align nonempty_interval.coe_one NonemptyInterval.coe_one #align nonempty_interval.coe_zero NonemptyInterval.coe_zero +-/ +#print NonemptyInterval.one_mem_one /- @[to_additive] theorem one_mem_one : (1 : α) ∈ (1 : NonemptyInterval α) := ⟨le_rfl, le_rfl⟩ #align nonempty_interval.one_mem_one NonemptyInterval.one_mem_one #align nonempty_interval.zero_mem_zero NonemptyInterval.zero_mem_zero +-/ end NonemptyInterval namespace Interval +#print Interval.coe_one /- @[simp, to_additive] theorem coe_one : ((1 : Interval α) : Set α) = 1 := Icc_self _ #align interval.coe_one Interval.coe_one #align interval.coe_zero Interval.coe_zero +-/ +#print Interval.one_mem_one /- @[to_additive] theorem one_mem_one : (1 : α) ∈ (1 : Interval α) := ⟨le_rfl, le_rfl⟩ #align interval.one_mem_one Interval.one_mem_one #align interval.zero_mem_zero Interval.zero_mem_zero +-/ end Interval @@ -171,35 +191,45 @@ namespace NonemptyInterval variable (s t : NonemptyInterval α) (a b : α) +#print NonemptyInterval.toProd_mul /- @[simp, to_additive to_prod_add] theorem toProd_mul : (s * t).toProd = s.toProd * t.toProd := rfl #align nonempty_interval.to_prod_mul NonemptyInterval.toProd_mul #align nonempty_interval.to_prod_add NonemptyInterval.toProd_add +-/ +#print NonemptyInterval.fst_mul /- @[to_additive] theorem fst_mul : (s * t).fst = s.fst * t.fst := rfl #align nonempty_interval.fst_mul NonemptyInterval.fst_mul #align nonempty_interval.fst_add NonemptyInterval.fst_add +-/ +#print NonemptyInterval.snd_mul /- @[to_additive] theorem snd_mul : (s * t).snd = s.snd * t.snd := rfl #align nonempty_interval.snd_mul NonemptyInterval.snd_mul #align nonempty_interval.snd_add NonemptyInterval.snd_add +-/ +#print NonemptyInterval.coe_mul_interval /- @[simp, to_additive] theorem coe_mul_interval : (↑(s * t) : Interval α) = s * t := rfl #align nonempty_interval.coe_mul_interval NonemptyInterval.coe_mul_interval #align nonempty_interval.coe_add_interval NonemptyInterval.coe_add_interval +-/ +#print NonemptyInterval.pure_mul_pure /- @[simp, to_additive] theorem pure_mul_pure : pure a * pure b = pure (a * b) := rfl #align nonempty_interval.pure_mul_pure NonemptyInterval.pure_mul_pure #align nonempty_interval.pure_add_pure NonemptyInterval.pure_add_pure +-/ end NonemptyInterval @@ -304,12 +334,14 @@ instance [OrderedCommMonoid α] : CommMonoid (Interval α) := namespace NonemptyInterval +#print NonemptyInterval.coe_pow_interval /- @[simp, to_additive] theorem coe_pow_interval [OrderedCommMonoid α] (s : NonemptyInterval α) (n : ℕ) : (↑(s ^ n) : Interval α) = s ^ n := map_pow (⟨coe, coe_one_interval, coe_mul_interval⟩ : NonemptyInterval α →* Interval α) _ _ #align nonempty_interval.coe_pow_interval NonemptyInterval.coe_pow_interval #align nonempty_interval.coe_nsmul_interval NonemptyInterval.coe_nsmul_interval +-/ end NonemptyInterval @@ -647,11 +679,13 @@ namespace NonemptyInterval variable (s t : NonemptyInterval α) (a : α) +#print NonemptyInterval.length /- /-- The length of an interval is its first component minus its second component. This measures the accuracy of the approximation by an interval. -/ def length : α := s.snd - s.fst #align nonempty_interval.length NonemptyInterval.length +-/ @[simp] theorem length_nonneg : 0 ≤ s.length := @@ -682,11 +716,13 @@ theorem length_add : (s + t).length = s.length + t.length := theorem length_sub : (s - t).length = s.length + t.length := by simp [sub_eq_add_neg] #align nonempty_interval.length_sub NonemptyInterval.length_sub +#print NonemptyInterval.length_sum /- @[simp] theorem length_sum (f : ι → NonemptyInterval α) (s : Finset ι) : (∑ i in s, f i).length = ∑ i in s, (f i).length := map_sum (⟨length, length_zero, length_add⟩ : NonemptyInterval α →+ α) _ _ #align nonempty_interval.length_sum NonemptyInterval.length_sum +-/ end NonemptyInterval @@ -694,12 +730,14 @@ namespace Interval variable (s t : Interval α) (a : α) +#print Interval.length /- /-- The length of an interval is its first component minus its second component. This measures the accuracy of the approximation by an interval. -/ def length : Interval α → α | ⊥ => 0 | (s : NonemptyInterval α) => s.length #align interval.length Interval.length +-/ @[simp] theorem length_nonneg : ∀ s : Interval α, 0 ≤ s.length @@ -733,10 +771,12 @@ theorem length_sub_le : (s - t).length ≤ s.length + t.length := by simpa [sub_eq_add_neg] using length_add_le s (-t) #align interval.length_sub_le Interval.length_sub_le +#print Interval.length_sum_le /- theorem length_sum_le (f : ι → Interval α) (s : Finset ι) : (∑ i in s, f i).length ≤ ∑ i in s, (f i).length := Finset.le_sum_of_subadditive _ length_zero length_add_le _ _ #align interval.length_sum_le Interval.length_sum_le +-/ end Interval diff --git a/Mathbin/Analysis/Calculus/Monotone.lean b/Mathbin/Analysis/Calculus/Monotone.lean index 9b08e8c828..0b502f284a 100644 --- a/Mathbin/Analysis/Calculus/Monotone.lean +++ b/Mathbin/Analysis/Calculus/Monotone.lean @@ -68,6 +68,7 @@ theorem tendsto_apply_add_mul_sq_div_sub {f : ℝ → ℝ} {x a c d : ℝ} {l : field_simp [sub_ne_zero.2 hy] #align tendsto_apply_add_mul_sq_div_sub tendsto_apply_add_mul_sq_div_sub +#print StieltjesFunction.ae_hasDerivAt /- /-- A Stieltjes function is almost everywhere differentiable, with derivative equal to the Radon-Nikodym derivative of the associated Stieltjes measure with respect to Lebesgue. -/ theorem StieltjesFunction.ae_hasDerivAt (f : StieltjesFunction) : @@ -145,7 +146,9 @@ theorem StieltjesFunction.ae_hasDerivAt (f : StieltjesFunction) : rw [hasDerivAt_iff_tendsto_slope, slope_fun_def_field, ← nhds_left'_sup_nhds_right', tendsto_sup] exact ⟨L4, L1⟩ #align stieltjes_function.ae_has_deriv_at StieltjesFunction.ae_hasDerivAt +-/ +#print Monotone.ae_hasDerivAt /- /-- A monotone function is almost everywhere differentiable, with derivative equal to the Radon-Nikodym derivative of the associated Stieltjes measure with respect to Lebesgue. -/ theorem Monotone.ae_hasDerivAt {f : ℝ → ℝ} (hf : Monotone f) : @@ -236,12 +239,16 @@ theorem Monotone.ae_hasDerivAt {f : ℝ → ℝ} (hf : Monotone f) : tendsto_sup] exact ⟨L2, L1⟩ #align monotone.ae_has_deriv_at Monotone.ae_hasDerivAt +-/ +#print Monotone.ae_differentiableAt /- /-- A monotone real function is differentiable Lebesgue-almost everywhere. -/ theorem Monotone.ae_differentiableAt {f : ℝ → ℝ} (hf : Monotone f) : ∀ᵐ x, DifferentiableAt ℝ f x := by filter_upwards [hf.ae_has_deriv_at] with x hx using hx.differentiable_at #align monotone.ae_differentiable_at Monotone.ae_differentiableAt +-/ +#print MonotoneOn.ae_differentiableWithinAt_of_mem /- /-- A real function which is monotone on a set is differentiable Lebesgue-almost everywhere on this set. This version does not assume that `s` is measurable. For a formulation with `volume.restrict s` assuming that `s` is measurable, see `monotone_on.ae_differentiable_within_at`. @@ -265,7 +272,9 @@ theorem MonotoneOn.ae_differentiableWithinAt_of_mem {f : ℝ → ℝ} {s : Set filter_upwards [self_mem_nhdsWithin, this] with y hy h'y exact gf ⟨hy, h'y.1.le, h'y.2.le⟩ #align monotone_on.ae_differentiable_within_at_of_mem MonotoneOn.ae_differentiableWithinAt_of_mem +-/ +#print MonotoneOn.ae_differentiableWithinAt /- /-- A real function which is monotone on a set is differentiable Lebesgue-almost everywhere on this set. This version assumes that `s` is measurable and uses `volume.restrict s`. For a formulation without measurability assumption, @@ -276,4 +285,5 @@ theorem MonotoneOn.ae_differentiableWithinAt {f : ℝ → ℝ} {s : Set ℝ} (hf rw [ae_restrict_iff' hs] exact hf.ae_differentiable_within_at_of_mem #align monotone_on.ae_differentiable_within_at MonotoneOn.ae_differentiableWithinAt +-/ diff --git a/Mathbin/FieldTheory/AbelRuffini.lean b/Mathbin/FieldTheory/AbelRuffini.lean index 26eddd8ef1..c47556daa4 100644 --- a/Mathbin/FieldTheory/AbelRuffini.lean +++ b/Mathbin/FieldTheory/AbelRuffini.lean @@ -109,7 +109,7 @@ theorem gal_x_pow_sub_one_isSolvable (n : ℕ) : IsSolvable (X ^ n - 1 : F[X]).G by intro σ lift n to ℕ+ using hn' - exact map_root_of_unity_eq_pow_self σ.to_alg_hom (rootsOfUnity.mkOfPowEq a ha) + exact map_rootsOfUnity_eq_pow_self σ.to_alg_hom (rootsOfUnity.mkOfPowEq a ha) obtain ⟨c, hc⟩ := key σ obtain ⟨d, hd⟩ := key τ rw [σ.mul_apply, τ.mul_apply, hc, τ.map_pow, hd, σ.map_pow, hc, ← pow_mul, pow_mul'] diff --git a/Mathbin/GroupTheory/SchurZassenhaus.lean b/Mathbin/GroupTheory/SchurZassenhaus.lean index 83fa7c2428..c7653324f1 100644 --- a/Mathbin/GroupTheory/SchurZassenhaus.lean +++ b/Mathbin/GroupTheory/SchurZassenhaus.lean @@ -38,6 +38,7 @@ open MulOpposite MulAction Subgroup.leftTransversals MemLeftTransversals variable {G : Type _} [Group G] (H : Subgroup G) [IsCommutative H] [FiniteIndex H] (α β : leftTransversals (H : Set G)) +#print Subgroup.QuotientDiff /- /-- The quotient of the transversals of an abelian normal `N` by the `diff` relation. -/ def QuotientDiff := Quotient @@ -45,6 +46,7 @@ def QuotientDiff := ⟨fun α => diff_self (MonoidHom.id H) α, fun α β h => by rw [← diff_inv, h, inv_one], fun α β γ h h' => by rw [← diff_mul_diff, h, h', one_mul]⟩) #align subgroup.quotient_diff Subgroup.QuotientDiff +-/ instance : Inhabited H.QuotientDiff := Quotient.inhabited _ diff --git a/Mathbin/LinearAlgebra/BilinearForm.lean b/Mathbin/LinearAlgebra/BilinearForm.lean index dd4f7d89fb..66ce1b174d 100644 --- a/Mathbin/LinearAlgebra/BilinearForm.lean +++ b/Mathbin/LinearAlgebra/BilinearForm.lean @@ -419,14 +419,12 @@ theorem toLin'_apply (A : BilinForm R M) (x : M) : ⇑(toLinHom R₂ A x) = A x rfl #align bilin_form.to_lin'_apply BilinForm.toLin'_apply -#print BilinForm.toLin' /- /-- The linear map obtained from a `bilin_form` by fixing the left co-ordinate and evaluating in the right. Over a commutative semiring, use `to_lin`, which is linear rather than `ℕ`-linear. -/ abbrev toLin' : BilinForm R M →ₗ[ℕ] M →ₗ[ℕ] M →ₗ[R] R := toLinHom ℕ #align bilin_form.to_lin' BilinForm.toLin' --/ @[simp] theorem sum_left {α} (t : Finset α) (g : α → M) (w : M) : @@ -461,14 +459,12 @@ theorem toLin'Flip_apply (A : BilinForm R M) (x : M) : ⇑(toLinHomFlip R₂ A x rfl #align bilin_form.to_lin'_flip_apply BilinForm.toLin'Flip_apply -#print BilinForm.toLin'Flip /- /-- The linear map obtained from a `bilin_form` by fixing the right co-ordinate and evaluating in the left. Over a commutative semiring, use `to_lin_flip`, which is linear rather than `ℕ`-linear. -/ abbrev toLin'Flip : BilinForm R M →ₗ[ℕ] M →ₗ[ℕ] M →ₗ[R] R := toLinHomFlip ℕ #align bilin_form.to_lin'_flip BilinForm.toLin'Flip --/ end ToLin' @@ -491,7 +487,6 @@ def LinearMap.toBilinAux (f : M₂ →ₗ[R₂] M₂ →ₗ[R₂] R₂) : BilinF #align linear_map.to_bilin_aux LinearMap.toBilinAux -/ -#print BilinForm.toLin /- /-- Bilinear forms are linearly equivalent to maps with two arguments that are linear in both. -/ def BilinForm.toLin : BilinForm R₂ M₂ ≃ₗ[R₂] M₂ →ₗ[R₂] M₂ →ₗ[R₂] R₂ := { BilinForm.toLinHom R₂ with @@ -499,14 +494,11 @@ def BilinForm.toLin : BilinForm R₂ M₂ ≃ₗ[R₂] M₂ →ₗ[R₂] M₂ left_inv := fun B => by ext; simp [LinearMap.toBilinAux] right_inv := fun B => by ext; simp [LinearMap.toBilinAux] } #align bilin_form.to_lin BilinForm.toLin --/ -#print LinearMap.toBilin /- /-- A map with two arguments that is linear in both is linearly equivalent to bilinear form. -/ def LinearMap.toBilin : (M₂ →ₗ[R₂] M₂ →ₗ[R₂] R₂) ≃ₗ[R₂] BilinForm R₂ M₂ := BilinForm.toLin.symm #align linear_map.to_bilin LinearMap.toBilin --/ @[simp] theorem LinearMap.toBilinAux_eq (f : M₂ →ₗ[R₂] M₂ →ₗ[R₂] R₂) : @@ -1430,7 +1422,6 @@ theorem iIsOrtho.nondegenerate_iff_not_isOrtho_basis_self {n : Type w} [Nontrivi section -#print BilinForm.toLin_restrict_ker_eq_inf_orthogonal /- theorem toLin_restrict_ker_eq_inf_orthogonal (B : BilinForm K V) (W : Subspace K V) (b : B.IsRefl) : (B.toLin.domRestrict W).ker.map W.Subtype = (W ⊓ B.orthogonal ⊤ : Subspace K V) := by @@ -1449,7 +1440,6 @@ theorem toLin_restrict_ker_eq_inf_orthogonal (B : BilinForm K V) (W : Subspace K rw [b] exact hx.2 _ Submodule.mem_top #align bilin_form.to_lin_restrict_ker_eq_inf_orthogonal BilinForm.toLin_restrict_ker_eq_inf_orthogonal --/ #print BilinForm.toLin_restrict_range_dualCoannihilator_eq_orthogonal /- theorem toLin_restrict_range_dualCoannihilator_eq_orthogonal (B : BilinForm K V) diff --git a/Mathbin/LinearAlgebra/Coevaluation.lean b/Mathbin/LinearAlgebra/Coevaluation.lean index 0354d40aaa..182ebfd497 100644 --- a/Mathbin/LinearAlgebra/Coevaluation.lean +++ b/Mathbin/LinearAlgebra/Coevaluation.lean @@ -45,7 +45,6 @@ variable (K : Type u) [Field K] variable (V : Type v) [AddCommGroup V] [Module K V] [FiniteDimensional K V] -#print coevaluation /- /-- The coevaluation map is a linear map from a field `K` to a finite dimensional vector space `V`. -/ def coevaluation : K →ₗ[K] V ⊗[K] Module.Dual K V := @@ -53,9 +52,7 @@ def coevaluation : K →ₗ[K] V ⊗[K] Module.Dual K V := (Basis.singleton Unit K).constr K fun _ => ∑ i : Basis.ofVectorSpaceIndex K V, bV i ⊗ₜ[K] bV.Coord i #align coevaluation coevaluation --/ -#print coevaluation_apply_one /- theorem coevaluation_apply_one : (coevaluation K V) (1 : K) = let bV := Basis.ofVectorSpace K V @@ -66,11 +63,9 @@ theorem coevaluation_apply_one : simp only [Fintype.univ_punit, Finset.sum_const, one_smul, Basis.singleton_repr, Basis.equivFun_apply, Basis.coe_ofVectorSpace, one_nsmul, Finset.card_singleton] #align coevaluation_apply_one coevaluation_apply_one --/ open TensorProduct -#print contractLeft_assoc_coevaluation /- /-- This lemma corresponds to one of the coherence laws for duals in rigid categories, see `category_theory.monoidal.rigid`. -/ theorem contractLeft_assoc_coevaluation : @@ -91,7 +86,6 @@ theorem contractLeft_assoc_coevaluation : simp only [Basis.coe_dualBasis, Basis.coord_apply, Basis.repr_self_apply, TensorProduct.ite_tmul] rw [Finset.sum_ite_eq']; simp only [Finset.mem_univ, if_true] #align contract_left_assoc_coevaluation contractLeft_assoc_coevaluation --/ /-- This lemma corresponds to one of the coherence laws for duals in rigid categories, see `category_theory.monoidal.rigid`. -/ diff --git a/Mathbin/LinearAlgebra/Contraction.lean b/Mathbin/LinearAlgebra/Contraction.lean index 4d54fc707c..8540961ecc 100644 --- a/Mathbin/LinearAlgebra/Contraction.lean +++ b/Mathbin/LinearAlgebra/Contraction.lean @@ -47,27 +47,21 @@ variable [Module R M] [Module R N] [Module R P] [Module R Q] variable [DecidableEq ι] [Fintype ι] (b : Basis ι R M) -#print contractLeft /- /-- The natural left-handed pairing between a module and its dual. -/ def contractLeft : Module.Dual R M ⊗ M →ₗ[R] R := (uncurry _ _ _ _).toFun LinearMap.id #align contract_left contractLeft --/ -#print contractRight /- /-- The natural right-handed pairing between a module and its dual. -/ def contractRight : M ⊗ Module.Dual R M →ₗ[R] R := (uncurry _ _ _ _).toFun (LinearMap.flip LinearMap.id) #align contract_right contractRight --/ -#print dualTensorHom /- /-- The natural map associating a linear map to the tensor product of two modules. -/ def dualTensorHom : Module.Dual R M ⊗ N →ₗ[R] M →ₗ[R] N := let M' := Module.Dual R M (uncurry R M' N (M →ₗ[R] N) : _ → M' ⊗ N →ₗ[R] M →ₗ[R] N) LinearMap.smulRightₗ #align dual_tensor_hom dualTensorHom --/ variable {R M N P Q} @@ -87,7 +81,6 @@ theorem dualTensorHom_apply (f : Module.Dual R M) (m : M) (n : N) : rfl #align dual_tensor_hom_apply dualTensorHom_apply -#print transpose_dualTensorHom /- @[simp] theorem transpose_dualTensorHom (f : Module.Dual R M) (m : M) : Dual.transpose (dualTensorHom R M M (f ⊗ₜ m)) = dualTensorHom R _ _ (Dual.eval R M m ⊗ₜ f) := @@ -97,7 +90,6 @@ theorem transpose_dualTensorHom (f : Module.Dual R M) (m : M) : LinearMap.map_smulₛₗ, RingHom.id_apply, Algebra.id.smul_eq_mul, dual.eval_apply, smul_apply] exact mul_comm _ _ #align transpose_dual_tensor_hom transpose_dualTensorHom --/ @[simp] theorem dualTensorHom_prodMap_zero (f : Module.Dual R M) (p : P) : @@ -164,7 +156,6 @@ variable [DecidableEq ι] [Fintype ι] (b : Basis ι R M) variable {R M N P Q} -#print dualTensorHomEquivOfBasis /- /-- If `M` is free, the natural linear map $M^* ⊗ N → Hom(M, N)$ is an equivalence. This function provides this equivalence in return for a basis of `M`. -/ @[simps apply] @@ -182,24 +173,19 @@ noncomputable def dualTensorHomEquivOfBasis : Module.Dual R M ⊗[R] N ≃ₗ[R] Fintype.sum_apply, Function.comp_apply, Basis.coe_dualBasis, coe_comp, compr₂_apply, tmul_smul, smul_tmul', ← sum_tmul, Basis.sum_dual_apply_smul_coord]) #align dual_tensor_hom_equiv_of_basis dualTensorHomEquivOfBasis --/ -#print dualTensorHomEquivOfBasis_toLinearMap /- @[simp] theorem dualTensorHomEquivOfBasis_toLinearMap : (dualTensorHomEquivOfBasis b : Module.Dual R M ⊗[R] N ≃ₗ[R] M →ₗ[R] N).toLinearMap = dualTensorHom R M N := rfl #align dual_tensor_hom_equiv_of_basis_to_linear_map dualTensorHomEquivOfBasis_toLinearMap --/ -#print dualTensorHomEquivOfBasis_symm_cancel_left /- @[simp] theorem dualTensorHomEquivOfBasis_symm_cancel_left (x : Module.Dual R M ⊗[R] N) : (dualTensorHomEquivOfBasis b).symm (dualTensorHom R M N x) = x := by rw [← dualTensorHomEquivOfBasis_apply b, LinearEquiv.symm_apply_apply] #align dual_tensor_hom_equiv_of_basis_symm_cancel_left dualTensorHomEquivOfBasis_symm_cancel_left --/ @[simp] theorem dualTensorHomEquivOfBasis_symm_cancel_right (x : M →ₗ[R] N) : @@ -213,14 +199,12 @@ variable [Module.Free R M] [Module.Finite R M] [Nontrivial R] open scoped Classical -#print dualTensorHomEquiv /- /-- If `M` is finite free, the natural map $M^* ⊗ N → Hom(M, N)$ is an equivalence. -/ @[simp] noncomputable def dualTensorHomEquiv : Module.Dual R M ⊗[R] N ≃ₗ[R] M →ₗ[R] N := dualTensorHomEquivOfBasis (Module.Free.chooseBasis R M) #align dual_tensor_hom_equiv dualTensorHomEquiv --/ end CommRing @@ -302,21 +286,17 @@ theorem rTensorHomEquivHomRTensor_toLinearMap : variable {R M N P Q} -#print lTensorHomEquivHomLTensor_apply /- @[simp] theorem lTensorHomEquivHomLTensor_apply (x : P ⊗[R] (M →ₗ[R] Q)) : lTensorHomEquivHomLTensor R M P Q x = lTensorHomToHomLTensor R M P Q x := by rw [← LinearEquiv.coe_toLinearMap, lTensorHomEquivHomLTensor_toLinearMap] #align ltensor_hom_equiv_hom_ltensor_apply lTensorHomEquivHomLTensor_apply --/ -#print rTensorHomEquivHomRTensor_apply /- @[simp] theorem rTensorHomEquivHomRTensor_apply (x : (M →ₗ[R] P) ⊗[R] Q) : rTensorHomEquivHomRTensor R M P Q x = rTensorHomToHomRTensor R M P Q x := by rw [← LinearEquiv.coe_toLinearMap, rTensorHomEquivHomRTensor_toLinearMap] #align rtensor_hom_equiv_hom_rtensor_apply rTensorHomEquivHomRTensor_apply --/ variable (R M N P Q) @@ -348,13 +328,11 @@ theorem homTensorHomEquiv_toLinearMap : variable {R M N P Q} -#print homTensorHomEquiv_apply /- @[simp] theorem homTensorHomEquiv_apply (x : (M →ₗ[R] P) ⊗[R] (N →ₗ[R] Q)) : homTensorHomEquiv R M N P Q x = homTensorHomMap R M N P Q x := by rw [← LinearEquiv.coe_toLinearMap, homTensorHomEquiv_toLinearMap] #align hom_tensor_hom_equiv_apply homTensorHomEquiv_apply --/ end CommRing diff --git a/Mathbin/LinearAlgebra/Dual.lean b/Mathbin/LinearAlgebra/Dual.lean index 68a6861a0c..1d86055df7 100644 --- a/Mathbin/LinearAlgebra/Dual.lean +++ b/Mathbin/LinearAlgebra/Dual.lean @@ -161,12 +161,10 @@ theorem transpose_apply (u : M →ₗ[R] M') (l : Dual R M') : transpose u l = l variable {M'' : Type _} [AddCommMonoid M''] [Module R M''] -#print Module.Dual.transpose_comp /- theorem transpose_comp (u : M' →ₗ[R] M'') (v : M →ₗ[R] M') : transpose (u.comp v) = (transpose v).comp (transpose u) := rfl #align module.dual.transpose_comp Module.Dual.transpose_comp --/ end Dual @@ -206,11 +204,9 @@ def LinearMap.dualMap (f : M₁ →ₗ[R] M₂) : Dual R M₂ →ₗ[R] Dual R M #align linear_map.dual_map LinearMap.dualMap -/ -#print LinearMap.dualMap_def /- theorem LinearMap.dualMap_def (f : M₁ →ₗ[R] M₂) : f.dualMap = Module.Dual.transpose f := rfl #align linear_map.dual_map_def LinearMap.dualMap_def --/ theorem LinearMap.dualMap_apply' (f : M₁ →ₗ[R] M₂) (g : Dual R M₂) : f.dualMap g = g.comp f := rfl @@ -374,13 +370,10 @@ theorem toDual_inj (m : M) (a : b.toDual m = 0) : m = 0 := rfl #align basis.to_dual_inj Basis.toDual_inj -#print Basis.toDual_ker /- theorem toDual_ker : b.toDual.ker = ⊥ := ker_eq_bot'.mpr b.toDual_inj #align basis.to_dual_ker Basis.toDual_ker --/ -#print Basis.toDual_range /- theorem toDual_range [Finite ι] : b.toDual.range = ⊤ := by cases nonempty_fintype ι @@ -391,7 +384,6 @@ theorem toDual_range [Finite ι] : b.toDual.range = ⊤ := rw [b.to_dual_eq_repr _ i, repr_total b] rfl #align basis.to_dual_range Basis.toDual_range --/ end CommSemiring @@ -570,10 +562,8 @@ section variable (K) (V) -#print Module.eval_ker /- theorem eval_ker : (eval K V).ker = ⊥ := by classical exact (Basis.ofVectorSpace K V).eval_ker #align module.eval_ker Module.eval_ker --/ #print Module.map_eval_injective /- theorem map_eval_injective : (Submodule.map (eval K V)).Injective := @@ -601,17 +591,13 @@ section variable (K) -#print Module.eval_apply_eq_zero_iff /- theorem eval_apply_eq_zero_iff (v : V) : (eval K V) v = 0 ↔ v = 0 := by simpa only using set_like.ext_iff.mp (eval_ker K V) v #align module.eval_apply_eq_zero_iff Module.eval_apply_eq_zero_iff --/ -#print Module.eval_apply_injective /- theorem eval_apply_injective : Function.Injective (eval K V) := (injective_iff_map_eq_zero' (eval K V)).mpr (eval_apply_eq_zero_iff K) #align module.eval_apply_injective Module.eval_apply_injective --/ theorem forall_dual_apply_eq_zero_iff (v : V) : (∀ φ : Module.Dual K V, φ v = 0) ↔ v = 0 := by rw [← eval_apply_eq_zero_iff K v, LinearMap.ext_iff]; rfl @@ -627,12 +613,10 @@ theorem dual_rank_eq [FiniteDimensional K V] : #align module.dual_rank_eq Module.dual_rank_eq -/ -#print Module.erange_coe /- theorem erange_coe [FiniteDimensional K V] : (eval K V).range = ⊤ := letI : IsNoetherian K V := IsNoetherian.iff_fg.2 inferInstance (Basis.ofVectorSpace K V).eval_range #align module.erange_coe Module.erange_coe --/ variable (K V) @@ -662,21 +646,17 @@ theorem evalEquiv_toLinearMap [FiniteDimensional K V] : #align module.eval_equiv_to_linear_map Module.evalEquiv_toLinearMap -/ -#print Module.mapEvalEquiv_apply /- @[simp] theorem mapEvalEquiv_apply [FiniteDimensional K V] (W : Subspace K V) : mapEvalEquiv K V W = W.map (eval K V) := rfl #align module.map_eval_equiv_apply Module.mapEvalEquiv_apply --/ -#print Module.mapEvalEquiv_symm_apply /- @[simp] theorem mapEvalEquiv_symm_apply [FiniteDimensional K V] (W'' : Subspace K (Dual K (Dual K V))) : (mapEvalEquiv K V).symm W'' = W''.comap (eval K V) := rfl #align module.map_eval_equiv_symm_apply Module.mapEvalEquiv_symm_apply --/ end Module @@ -877,12 +857,10 @@ def dualCoannihilator (Φ : Submodule R (Module.Dual R M)) : Submodule R M := #align submodule.dual_coannihilator Submodule.dualCoannihilator -/ -#print Submodule.mem_dualCoannihilator /- theorem mem_dualCoannihilator {Φ : Submodule R (Module.Dual R M)} (x : M) : x ∈ Φ.dualCoannihilator ↔ ∀ φ ∈ Φ, (φ x : R) = 0 := by simp_rw [dual_coannihilator, mem_comap, mem_dual_annihilator, Module.Dual.eval_apply] #align submodule.mem_dual_coannihilator Submodule.mem_dualCoannihilator --/ theorem dualAnnihilator_gc (R M : Type _) [CommSemiring R] [AddCommMonoid M] [Module R M] : GaloisConnection @@ -908,14 +886,11 @@ theorem le_dualAnnihilator_iff_le_dualCoannihilator {U : Submodule R (Module.Dua #align submodule.le_dual_annihilator_iff_le_dual_coannihilator Submodule.le_dualAnnihilator_iff_le_dualCoannihilator -/ -#print Submodule.dualAnnihilator_bot /- @[simp] theorem dualAnnihilator_bot : (⊥ : Submodule R M).dualAnnihilator = ⊤ := (dualAnnihilator_gc R M).l_bot #align submodule.dual_annihilator_bot Submodule.dualAnnihilator_bot --/ -#print Submodule.dualAnnihilator_top /- @[simp] theorem dualAnnihilator_top : (⊤ : Submodule R M).dualAnnihilator = ⊥ := by @@ -924,14 +899,11 @@ theorem dualAnnihilator_top : (⊤ : Submodule R M).dualAnnihilator = ⊥ := simp_rw [mem_dual_annihilator, mem_bot, mem_top, forall_true_left] exact fun h => LinearMap.ext h #align submodule.dual_annihilator_top Submodule.dualAnnihilator_top --/ -#print Submodule.dualCoannihilator_bot /- @[simp] theorem dualCoannihilator_bot : (⊥ : Submodule R (Module.Dual R M)).dualCoannihilator = ⊤ := (dualAnnihilator_gc R M).u_top #align submodule.dual_coannihilator_bot Submodule.dualCoannihilator_bot --/ #print Submodule.dualAnnihilator_anti /- @[mono] @@ -977,19 +949,15 @@ theorem dualCoannihilator_dualAnnihilator_dualCoannihilator (U : Submodule R (Mo #align submodule.dual_coannihilator_dual_annihilator_dual_coannihilator Submodule.dualCoannihilator_dualAnnihilator_dualCoannihilator -/ -#print Submodule.dualAnnihilator_sup_eq /- theorem dualAnnihilator_sup_eq (U V : Submodule R M) : (U ⊔ V).dualAnnihilator = U.dualAnnihilator ⊓ V.dualAnnihilator := (dualAnnihilator_gc R M).l_sup #align submodule.dual_annihilator_sup_eq Submodule.dualAnnihilator_sup_eq --/ -#print Submodule.dualCoannihilator_sup_eq /- theorem dualCoannihilator_sup_eq (U V : Submodule R (Module.Dual R M)) : (U ⊔ V).dualCoannihilator = U.dualCoannihilator ⊓ V.dualCoannihilator := (dualAnnihilator_gc R M).u_inf #align submodule.dual_coannihilator_sup_eq Submodule.dualCoannihilator_sup_eq --/ theorem dualAnnihilator_iSup_eq {ι : Type _} (U : ι → Submodule R M) : (⨆ i : ι, U i).dualAnnihilator = ⨅ i : ι, (U i).dualAnnihilator := @@ -1001,7 +969,6 @@ theorem dualCoannihilator_iSup_eq {ι : Type _} (U : ι → Submodule R (Module. (dualAnnihilator_gc R M).u_iInf #align submodule.dual_coannihilator_supr_eq Submodule.dualCoannihilator_iSup_eq -#print Submodule.sup_dualAnnihilator_le_inf /- /-- See also `subspace.dual_annihilator_inf_eq` for vector subspaces. -/ theorem sup_dualAnnihilator_le_inf (U V : Submodule R M) : U.dualAnnihilator ⊔ V.dualAnnihilator ≤ (U ⊓ V).dualAnnihilator := @@ -1009,7 +976,6 @@ theorem sup_dualAnnihilator_le_inf (U V : Submodule R M) : rw [le_dual_annihilator_iff_le_dual_coannihilator, dual_coannihilator_sup_eq] apply inf_le_inf <;> exact le_dual_annihilator_dual_coannihilator _ #align submodule.sup_dual_annihilator_le_inf Submodule.sup_dualAnnihilator_le_inf --/ /-- See also `subspace.dual_annihilator_infi_eq` for vector subspaces when `ι` is finite. -/ theorem iSup_dualAnnihilator_le_iInf {ι : Type _} (U : ι → Submodule R M) : @@ -1031,13 +997,11 @@ universe u v w -- We work in vector spaces because `exists_is_compl` only hold for vector spaces variable {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] -#print Subspace.dualCoannihilator_top /- @[simp] theorem dualCoannihilator_top (W : Subspace K V) : (⊤ : Subspace K (Module.Dual K W)).dualCoannihilator = ⊥ := by rw [dual_coannihilator, dual_annihilator_top, comap_bot, Module.eval_ker] #align subspace.dual_coannihilator_top Subspace.dualCoannihilator_top --/ #print Subspace.dualAnnihilator_dualCoannihilator_eq /- theorem dualAnnihilator_dualCoannihilator_eq {W : Subspace K V} : @@ -1194,7 +1158,6 @@ instance [H : FiniteDimensional K V] : FiniteDimensional K (Module.Dual K V) := variable [FiniteDimensional K V] [FiniteDimensional K V₁] -#print Subspace.dualAnnihilator_dualAnnihilator_eq /- theorem dualAnnihilator_dualAnnihilator_eq (W : Subspace K V) : W.dualAnnihilator.dualAnnihilator = Module.mapEvalEquiv K V W := by @@ -1202,7 +1165,6 @@ theorem dualAnnihilator_dualAnnihilator_eq (W : Subspace K V) : rw [dual_coannihilator, ← Module.mapEvalEquiv_symm_apply] at this rwa [← OrderIso.symm_apply_eq] #align subspace.dual_annihilator_dual_annihilator_eq Subspace.dualAnnihilator_dualAnnihilator_eq --/ #print Subspace.dual_finrank_eq /- -- TODO(kmill): https://github.com/leanprover-community/mathlib/pull/17521#discussion_r1083241963 @@ -1649,7 +1611,6 @@ variable [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] variable [Module R M] [Module R N] -#print TensorProduct.dualDistrib /- /-- The canonical linear map from `dual M ⊗ dual N` to `dual (M ⊗ N)`, sending `f ⊗ g` to the composition of `tensor_product.map f g` with the natural isomorphism `R ⊗ R ≃ R`. @@ -1657,7 +1618,6 @@ the natural isomorphism `R ⊗ R ≃ R`. def dualDistrib : Dual R M ⊗[R] Dual R N →ₗ[R] Dual R (M ⊗[R] N) := compRight ↑(TensorProduct.lid R R) ∘ₗ homTensorHomMap R M N R R #align tensor_product.dual_distrib TensorProduct.dualDistrib --/ variable {R M N} @@ -1692,7 +1652,6 @@ theorem dualDistribInvOfBasis_apply (b : Basis ι R M) (c : Basis κ R N) (f : D simp [dual_distrib_inv_of_basis] #align tensor_product.dual_distrib_inv_of_basis_apply TensorProduct.dualDistribInvOfBasis_apply -#print TensorProduct.dualDistribEquivOfBasis /- /-- A linear equivalence between `dual M ⊗ dual N` and `dual (M ⊗ N)` given bases for `M` and `N`. It sends `f ⊗ g` to the composition of `tensor_product.map f g` with the natural isomorphism `R ⊗ R ≃ R`. @@ -1713,7 +1672,6 @@ noncomputable def dualDistribEquivOfBasis (b : Basis ι R M) (c : Basis κ R N) dual_distrib_apply, ← smul_tmul_smul, ← tmul_sum, ← sum_tmul, Basis.coe_dualBasis, Basis.sum_dual_apply_smul_coord] #align tensor_product.dual_distrib_equiv_of_basis TensorProduct.dualDistribEquivOfBasis --/ variable (R M N) @@ -1723,7 +1681,6 @@ variable [Nontrivial R] open scoped Classical -#print TensorProduct.dualDistribEquiv /- /-- A linear equivalence between `dual M ⊗ dual N` and `dual (M ⊗ N)` when `M` and `N` are finite free modules. It sends `f ⊗ g` to the composition of `tensor_product.map f g` with the natural @@ -1733,7 +1690,6 @@ isomorphism `R ⊗ R ≃ R`. noncomputable def dualDistribEquiv : Dual R M ⊗[R] Dual R N ≃ₗ[R] Dual R (M ⊗[R] N) := dualDistribEquivOfBasis (Module.Free.chooseBasis R M) (Module.Free.chooseBasis R N) #align tensor_product.dual_distrib_equiv TensorProduct.dualDistribEquiv --/ end TensorProduct diff --git a/Mathbin/LinearAlgebra/Matrix/SesquilinearForm.lean b/Mathbin/LinearAlgebra/Matrix/SesquilinearForm.lean index 0b684523e0..667e0173d0 100644 --- a/Mathbin/LinearAlgebra/Matrix/SesquilinearForm.lean +++ b/Mathbin/LinearAlgebra/Matrix/SesquilinearForm.lean @@ -729,22 +729,18 @@ theorem Matrix.separatingLeft_toLinearMap₂'_iff_separatingLeft_toLinearMap₂ variable (B : M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁) -#print Matrix.Nondegenerate.toLinearMap₂' /- -- Lemmas transferring nondegeneracy between a matrix and its associated bilinear form theorem Matrix.Nondegenerate.toLinearMap₂' {M : Matrix ι ι R₁} (h : M.Nondegenerate) : M.toLinearMap₂'.SeparatingLeft := fun x hx => h.eq_zero_of_ortho fun y => by simpa only [to_linear_map₂'_apply'] using hx y #align matrix.nondegenerate.to_linear_map₂' Matrix.Nondegenerate.toLinearMap₂' --/ -#print Matrix.separatingLeft_toLinearMap₂'_iff /- @[simp] theorem Matrix.separatingLeft_toLinearMap₂'_iff {M : Matrix ι ι R₁} : M.toLinearMap₂'.SeparatingLeft ↔ M.Nondegenerate := ⟨fun h v hv => h v fun w => (M.toLinearMap₂'_apply' _ _).trans <| hv w, Matrix.Nondegenerate.toLinearMap₂'⟩ #align matrix.separating_left_to_linear_map₂'_iff Matrix.separatingLeft_toLinearMap₂'_iff --/ theorem Matrix.Nondegenerate.toLinearMap₂ {M : Matrix ι ι R₁} (h : M.Nondegenerate) (b : Basis ι R₁ M₁) : (toLinearMap₂ b b M).SeparatingLeft := @@ -786,12 +782,10 @@ theorem SeparatingLeft.toMatrix₂ {B : M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁ -- Some shorthands for combining the above with `matrix.nondegenerate_of_det_ne_zero` variable [IsDomain R₁] -#print LinearMap.separatingLeft_toLinearMap₂'_iff_det_ne_zero /- theorem separatingLeft_toLinearMap₂'_iff_det_ne_zero {M : Matrix ι ι R₁} : M.toLinearMap₂'.SeparatingLeft ↔ M.det ≠ 0 := by rw [Matrix.separatingLeft_toLinearMap₂'_iff, Matrix.nondegenerate_iff_det_ne_zero] #align linear_map.separating_left_to_linear_map₂'_iff_det_ne_zero LinearMap.separatingLeft_toLinearMap₂'_iff_det_ne_zero --/ theorem separatingLeft_toLinearMap₂'_of_det_ne_zero' (M : Matrix ι ι R₁) (h : M.det ≠ 0) : M.toLinearMap₂'.SeparatingLeft := diff --git a/Mathbin/MeasureTheory/Covering/Besicovitch.lean b/Mathbin/MeasureTheory/Covering/Besicovitch.lean index d0d4588613..0969113995 100644 --- a/Mathbin/MeasureTheory/Covering/Besicovitch.lean +++ b/Mathbin/MeasureTheory/Covering/Besicovitch.lean @@ -113,6 +113,7 @@ open scoped Topology Classical BigOperators ENNReal MeasureTheory NNReal -/ +#print Besicovitch.SatelliteConfig /- /-- A satellite configuration is a configuration of `N+1` points that shows up in the inductive construction for the Besicovitch covering theorem. It depends on some parameter `τ ≥ 1`. @@ -135,7 +136,9 @@ structure Besicovitch.SatelliteConfig (α : Type _) [MetricSpace α] (N : ℕ) ( hlast : ∀ i < last N, r i ≤ dist (c i) (c (last N)) ∧ r (last N) ≤ τ * r i inter : ∀ i < last N, dist (c i) (c (last N)) ≤ r i + r (last N) #align besicovitch.satellite_config Besicovitch.SatelliteConfig +-/ +#print HasBesicovitchCovering /- /- ./././Mathport/Syntax/Translate/Command.lean:394:30: infer kinds are unsupported in Lean 4: #[`no_satelliteConfig] [] -/ /-- A metric space has the Besicovitch covering property if there exist `N` and `τ > 1` such that there are no satellite configuration of parameter `τ` with `N+1` points. This is the condition that @@ -144,6 +147,7 @@ finite-dimensional real vector spaces. -/ class HasBesicovitchCovering (α : Type _) [MetricSpace α] : Prop where no_satelliteConfig : ∃ (N : ℕ) (τ : ℝ), 1 < τ ∧ IsEmpty (Besicovitch.SatelliteConfig α N τ) #align has_besicovitch_covering HasBesicovitchCovering +-/ /-- There is always a satellite configuration with a single point. -/ instance {α : Type _} {τ : ℝ} [Inhabited α] [MetricSpace α] : @@ -185,28 +189,33 @@ end SatelliteConfig /-! ### Extracting disjoint subfamilies from a ball covering -/ +#print Besicovitch.BallPackage /- /-- A ball package is a family of balls in a metric space with positive bounded radii. -/ structure BallPackage (β : Type _) (α : Type _) where c : β → α R : β → ℝ rpos : ∀ b, 0 < r b - rBound : ℝ + r_bound : ℝ r_le : ∀ b, r b ≤ r_bound #align besicovitch.ball_package Besicovitch.BallPackage +-/ +#print Besicovitch.unitBallPackage /- /-- The ball package made of unit balls. -/ def unitBallPackage (α : Type _) : BallPackage α α where c := id R _ := 1 rpos _ := zero_lt_one - rBound := 1 + r_bound := 1 r_le _ := le_rfl #align besicovitch.unit_ball_package Besicovitch.unitBallPackage +-/ instance (α : Type _) : Inhabited (BallPackage α α) := ⟨unitBallPackage α⟩ +#print Besicovitch.TauPackage /- /-- A Besicovitch tau-package is a family of balls in a metric space with positive bounded radii, together with enough data to proceed with the Besicovitch greedy algorithm. We register this in a single structure to make sure that all our constructions in this algorithm only depend on @@ -215,6 +224,7 @@ structure TauPackage (β : Type _) (α : Type _) extends BallPackage β α where τ : ℝ one_lt_tau : 1 < τ #align besicovitch.tau_package Besicovitch.TauPackage +-/ instance (α : Type _) : Inhabited (TauPackage α α) := ⟨{ unitBallPackage α with @@ -229,6 +239,7 @@ variable [Nonempty β] (p : TauPackage β α) include p +#print Besicovitch.TauPackage.index /- /-- Choose inductively large balls with centers that are not contained in the union of already chosen balls. This is a transfinite induction. -/ noncomputable def index : Ordinal.{u} → β @@ -245,24 +256,30 @@ noncomputable def index : Ordinal.{u} → β fun b : β => p.c b ∉ Z ∧ R ≤ p.τ * p.R b decreasing_by exact j.2 #align besicovitch.tau_package.index Besicovitch.TauPackage.index +-/ +#print Besicovitch.TauPackage.iUnionUpTo /- /-- The set of points that are covered by the union of balls selected at steps `< i`. -/ -def unionUpTo (i : Ordinal.{u}) : Set α := +def iUnionUpTo (i : Ordinal.{u}) : Set α := ⋃ j : { j // j < i }, ball (p.c (p.index j)) (p.R (p.index j)) -#align besicovitch.tau_package.Union_up_to Besicovitch.TauPackage.unionUpTo +#align besicovitch.tau_package.Union_up_to Besicovitch.TauPackage.iUnionUpTo +-/ -theorem monotone_unionUpTo : Monotone p.unionUpTo := +theorem monotone_iUnionUpTo : Monotone p.iUnionUpTo := by intro i j hij simp only [Union_up_to] exact Union_mono' fun r => ⟨⟨r, r.2.trans_le hij⟩, subset.rfl⟩ -#align besicovitch.tau_package.monotone_Union_up_to Besicovitch.TauPackage.monotone_unionUpTo +#align besicovitch.tau_package.monotone_Union_up_to Besicovitch.TauPackage.monotone_iUnionUpTo +#print Besicovitch.TauPackage.R /- /-- Supremum of the radii of balls whose centers are not yet covered at step `i`. -/ -def r (i : Ordinal.{u}) : ℝ := - iSup fun b : { b : β // p.c b ∉ p.unionUpTo i } => p.R b -#align besicovitch.tau_package.R Besicovitch.TauPackage.r +def R (i : Ordinal.{u}) : ℝ := + iSup fun b : { b : β // p.c b ∉ p.iUnionUpTo i } => p.R b +#align besicovitch.tau_package.R Besicovitch.TauPackage.R +-/ +#print Besicovitch.TauPackage.color /- /-- Group the balls into disjoint families, by assigning to a ball the smallest color for which it does not intersect any already chosen ball of this color. -/ noncomputable def color : Ordinal.{u} → ℕ @@ -275,14 +292,17 @@ noncomputable def color : Ordinal.{u} → ℕ sInf (univ \ A) decreasing_by exact j.2 #align besicovitch.tau_package.color Besicovitch.TauPackage.color +-/ +#print Besicovitch.TauPackage.lastStep /- /-- `p.last_step` is the first ordinal where the construction stops making sense, i.e., `f` returns garbage since there is no point left to be chosen. We will only use ordinals before this step. -/ def lastStep : Ordinal.{u} := - sInf {i | ¬∃ b : β, p.c b ∉ p.unionUpTo i ∧ p.r i ≤ p.τ * p.R b} + sInf {i | ¬∃ b : β, p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.R b} #align besicovitch.tau_package.last_step Besicovitch.TauPackage.lastStep +-/ -theorem last_step_nonempty : {i | ¬∃ b : β, p.c b ∉ p.unionUpTo i ∧ p.r i ≤ p.τ * p.R b}.Nonempty := +theorem lastStep_nonempty : {i | ¬∃ b : β, p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.R b}.Nonempty := by by_contra suffices H : Function.Injective p.index; exact not_injective_of_ordinal p.index H @@ -305,10 +325,10 @@ theorem last_step_nonempty : {i | ¬∃ b : β, p.c b ∉ p.unionUpTo i ∧ p.r specialize A x H simp [hxy] at A exact (lt_irrefl _ ((p.rpos (p.index y)).trans_le A)).elim -#align besicovitch.tau_package.last_step_nonempty Besicovitch.TauPackage.last_step_nonempty +#align besicovitch.tau_package.last_step_nonempty Besicovitch.TauPackage.lastStep_nonempty /-- Every point is covered by chosen balls, before `p.last_step`. -/ -theorem mem_unionUpTo_lastStep (x : β) : p.c x ∈ p.unionUpTo p.lastStep := +theorem mem_iUnionUpTo_lastStep (x : β) : p.c x ∈ p.iUnionUpTo p.lastStep := by have A : ∀ z : β, p.c z ∈ p.Union_up_to p.last_step ∨ p.τ * p.r z < p.R p.last_step := by @@ -335,7 +355,7 @@ theorem mem_unionUpTo_lastStep (x : β) : p.c x ∈ p.unionUpTo p.lastStep := · rw [← div_eq_inv_mul] at hy2 have := (div_le_iff' (_root_.zero_lt_one.trans p.one_lt_tau)).1 hy2.le exact lt_irrefl _ (Hy.trans_le this) -#align besicovitch.tau_package.mem_Union_up_to_last_step Besicovitch.TauPackage.mem_unionUpTo_lastStep +#align besicovitch.tau_package.mem_Union_up_to_last_step Besicovitch.TauPackage.mem_iUnionUpTo_lastStep /-- If there are no configurations of satellites with `N+1` points, one never uses more than `N` distinct families in the Besicovitch inductive construction. -/ @@ -585,7 +605,7 @@ theorem exist_finset_disjoint_balls_large_measure (μ : Measure α) [IsFiniteMea { c := fun x => x R := fun x => r x rpos := fun x => rpos x x.2 - rBound := 1 + r_bound := 1 r_le := fun x => rle x x.2 } rcases exist_disjoint_covering_families hτ hN a with ⟨u, hu, hu'⟩ have u_count : ∀ i, (u i).Countable := by @@ -701,7 +721,7 @@ For a version assuming that the measure is sigma-finite, see `exists_disjoint_closed_ball_covering_ae_aux`. For a version giving the conclusion in a nicer form, see `exists_disjoint_closed_ball_covering_ae`. -/ -theorem exists_disjoint_closedBall_covering_ae_of_finite_measure_aux (μ : Measure α) +theorem exists_disjoint_closedBall_covering_ae_of_finiteMeasure_aux (μ : Measure α) [IsFiniteMeasure μ] (f : α → Set ℝ) (s : Set α) (hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty) : ∃ t : Set (α × ℝ), @@ -845,7 +865,7 @@ theorem exists_disjoint_closedBall_covering_ae_of_finite_measure_aux (μ : Measu apply (monotone_nat_of_le_succ fun n => _).directed_le rw [u_succ] exact (hF (u n) (Pu n)).1 -#align besicovitch.exists_disjoint_closed_ball_covering_ae_of_finite_measure_aux Besicovitch.exists_disjoint_closedBall_covering_ae_of_finite_measure_aux +#align besicovitch.exists_disjoint_closed_ball_covering_ae_of_finite_measure_aux Besicovitch.exists_disjoint_closedBall_covering_ae_of_finiteMeasure_aux /-- The measurable Besicovitch covering theorem. Assume that, for any `x` in a set `s`, one is given a set of admissible closed balls centered at `x`, with arbitrarily small radii. @@ -1009,7 +1029,7 @@ theorem exists_closedBall_covering_tsum_measure_le (μ : Measure α) [SigmaFinit { c := fun x => x R := fun x => r1 x rpos := fun x => (hr1 x.1 x.2).1.2.1 - rBound := 1 + r_bound := 1 r_le := fun x => (hr1 x.1 x.2).1.2.2.le } -- by Besicovitch, we cover `s'` with at most `N` families of disjoint balls, all included in -- a suitable neighborhood `v` of `s'`. @@ -1140,6 +1160,7 @@ theorem exists_closedBall_covering_tsum_measure_le (μ : Measure α) [SigmaFinit /-! ### Consequences on differentiation of measures -/ +#print Besicovitch.vitaliFamily /- /-- In a space with the Besicovitch covering property, the set of closed balls with positive radius forms a Vitali family. This is essentially a restatement of the measurable Besicovitch theorem. -/ protected def vitaliFamily (μ : Measure α) [SigmaFinite μ] : VitaliFamily μ @@ -1187,6 +1208,7 @@ protected def vitaliFamily (μ : Measure α) [SigmaFinite μ] : VitaliFamily μ · rintro - ⟨x, hx, rfl⟩; exact (tg x hx).1.2 · rwa [bUnion_image] #align besicovitch.vitali_family Besicovitch.vitaliFamily +-/ /-- The main feature of the Besicovitch Vitali family is that its filter at a point `x` corresponds to convergence along closed balls. We record one of the two implications here, which will enable us @@ -1238,6 +1260,7 @@ theorem ae_tendsto_measure_inter_div_of_measurableSet (μ : Measure β) [IsLocal exact hx.comp (tendsto_filter_at μ x) #align besicovitch.ae_tendsto_measure_inter_div_of_measurable_set Besicovitch.ae_tendsto_measure_inter_div_of_measurableSet +#print Besicovitch.ae_tendsto_measure_inter_div /- /-- Given an arbitrary set `s`, then `μ (s ∩ closed_ball x r) / μ (closed_ball x r)` converges to `1` when `r` tends to `0`, for almost every `x` in `s`. This shows that almost every point of `s` is a Lebesgue density point for `s`. @@ -1251,6 +1274,7 @@ theorem ae_tendsto_measure_inter_div (μ : Measure β) [IsLocallyFiniteMeasure filter_upwards [VitaliFamily.ae_tendsto_measure_inter_div (Besicovitch.vitaliFamily μ)] with x hx using hx.comp (tendsto_filter_at μ x) #align besicovitch.ae_tendsto_measure_inter_div Besicovitch.ae_tendsto_measure_inter_div +-/ end Besicovitch diff --git a/Mathbin/MeasureTheory/Covering/DensityTheorem.lean b/Mathbin/MeasureTheory/Covering/DensityTheorem.lean index 39026b4349..ab86863a54 100644 --- a/Mathbin/MeasureTheory/Covering/DensityTheorem.lean +++ b/Mathbin/MeasureTheory/Covering/DensityTheorem.lean @@ -49,6 +49,7 @@ variable [SecondCountableTopology α] [BorelSpace α] [IsLocallyFiniteMeasure μ open scoped Topology +#print IsUnifLocDoublingMeasure.vitaliFamily /- /-- A Vitali family in a space with a uniformly locally doubling measure, designed so that the sets at `x` contain all `closed_ball y r` when `dist x y ≤ K * r`. -/ irreducible_def vitaliFamily (K : ℝ) : VitaliFamily μ := @@ -74,6 +75,7 @@ irreducible_def vitaliFamily (K : ℝ) : VitaliFamily μ := (Vitali.vitaliFamily μ (scaling_constant_of μ (max (4 * K + 3) 3)) A).enlarge (R / 4) (by linarith) #align is_unif_loc_doubling_measure.vitali_family IsUnifLocDoublingMeasure.vitaliFamily +-/ /-- In the Vitali family `is_unif_loc_doubling_measure.vitali_family K`, the sets based at `x` contain all balls `closed_ball y r` when `dist x y ≤ K * r`. -/ diff --git a/Mathbin/MeasureTheory/Covering/OneDim.lean b/Mathbin/MeasureTheory/Covering/OneDim.lean index 636e6e0851..92cbb22b56 100644 --- a/Mathbin/MeasureTheory/Covering/OneDim.lean +++ b/Mathbin/MeasureTheory/Covering/OneDim.lean @@ -34,6 +34,7 @@ theorem Icc_mem_vitaliFamily_at_right {x y : ℝ} (hxy : x < y) : rw [dist_comm, Real.dist_eq, abs_of_nonneg] <;> linarith #align real.Icc_mem_vitali_family_at_right Real.Icc_mem_vitaliFamily_at_right +#print Real.tendsto_Icc_vitaliFamily_right /- theorem tendsto_Icc_vitaliFamily_right (x : ℝ) : Tendsto (fun y => Icc x y) (𝓝[>] x) ((VitaliFamily (volume : Measure ℝ) 1).filterAt x) := by @@ -45,6 +46,7 @@ theorem tendsto_Icc_vitaliFamily_right (x : ℝ) : rw [closed_ball_eq_Icc] exact Icc_subset_Icc (by linarith) hy.2 #align real.tendsto_Icc_vitali_family_right Real.tendsto_Icc_vitaliFamily_right +-/ theorem Icc_mem_vitaliFamily_at_left {x y : ℝ} (hxy : x < y) : Icc x y ∈ (VitaliFamily (volume : Measure ℝ) 1).setsAt y := @@ -54,6 +56,7 @@ theorem Icc_mem_vitaliFamily_at_left {x y : ℝ} (hxy : x < y) : rw [Real.dist_eq, abs_of_nonneg] <;> linarith #align real.Icc_mem_vitali_family_at_left Real.Icc_mem_vitaliFamily_at_left +#print Real.tendsto_Icc_vitaliFamily_left /- theorem tendsto_Icc_vitaliFamily_left (x : ℝ) : Tendsto (fun y => Icc y x) (𝓝[<] x) ((VitaliFamily (volume : Measure ℝ) 1).filterAt x) := by @@ -65,6 +68,7 @@ theorem tendsto_Icc_vitaliFamily_left (x : ℝ) : rw [closed_ball_eq_Icc] exact Icc_subset_Icc hy.1 (by linarith) #align real.tendsto_Icc_vitali_family_left Real.tendsto_Icc_vitaliFamily_left +-/ end Real diff --git a/Mathbin/MeasureTheory/Integral/FundThmCalculus.lean b/Mathbin/MeasureTheory/Integral/FundThmCalculus.lean index de9d8edb86..2849ba1f9f 100644 --- a/Mathbin/MeasureTheory/Integral/FundThmCalculus.lean +++ b/Mathbin/MeasureTheory/Integral/FundThmCalculus.lean @@ -189,6 +189,7 @@ In the next subsection we apply this theorem to prove various theorems about dif of the integral w.r.t. Lebesgue measure. -/ +#print intervalIntegral.FTCFilter /- /-- An auxiliary typeclass for the Fundamental theorem of calculus, part 1. It is used to formulate theorems that work simultaneously for left and right one-sided derivatives of `∫ x in u..v, f x`. -/ class FTCFilter (a : outParam ℝ) (outer : Filter ℝ) (inner : outParam <| Filter ℝ) extends @@ -197,6 +198,7 @@ class FTCFilter (a : outParam ℝ) (outer : Filter ℝ) (inner : outParam <| Fil le_nhds : inner ≤ 𝓝 a [meas_gen : IsMeasurablyGenerated inner] #align interval_integral.FTC_filter intervalIntegral.FTCFilter +-/ /- The `dangerous_instance` linter doesn't take `out_param`s into account, so it thinks that `FTC_filter.to_tendsto_Ixx_class` is dangerous. Disable this linter using `nolint`. @@ -215,42 +217,56 @@ instance nhdsWithinSingleton (a : ℝ) : FTCFilter a (𝓝[{a}] a) ⊥ := by rw [nhdsWithin, principal_singleton, inf_eq_right.2 (pure_le_nhds a)]; infer_instance #align interval_integral.FTC_filter.nhds_within_singleton intervalIntegral.FTCFilter.nhdsWithinSingleton +#print intervalIntegral.FTCFilter.finite_at_inner /- theorem finite_at_inner {a : ℝ} (l : Filter ℝ) {l'} [h : FTCFilter a l l'] {μ : Measure ℝ} [IsLocallyFiniteMeasure μ] : μ.FiniteAtFilter l' := (μ.finiteAtNhds a).filter_mono h.le_nhds #align interval_integral.FTC_filter.finite_at_inner intervalIntegral.FTCFilter.finite_at_inner +-/ +#print intervalIntegral.FTCFilter.nhds /- instance nhds (a : ℝ) : FTCFilter a (𝓝 a) (𝓝 a) where pure_le := pure_le_nhds a le_nhds := le_rfl #align interval_integral.FTC_filter.nhds intervalIntegral.FTCFilter.nhds +-/ +#print intervalIntegral.FTCFilter.nhdsUniv /- instance nhdsUniv (a : ℝ) : FTCFilter a (𝓝[univ] a) (𝓝 a) := by rw [nhdsWithin_univ]; infer_instance #align interval_integral.FTC_filter.nhds_univ intervalIntegral.FTCFilter.nhdsUniv +-/ +#print intervalIntegral.FTCFilter.nhdsLeft /- instance nhdsLeft (a : ℝ) : FTCFilter a (𝓝[≤] a) (𝓝[≤] a) where pure_le := pure_le_nhdsWithin right_mem_Iic le_nhds := inf_le_left #align interval_integral.FTC_filter.nhds_left intervalIntegral.FTCFilter.nhdsLeft +-/ +#print intervalIntegral.FTCFilter.nhdsRight /- instance nhdsRight (a : ℝ) : FTCFilter a (𝓝[≥] a) (𝓝[>] a) where pure_le := pure_le_nhdsWithin left_mem_Ici le_nhds := inf_le_left #align interval_integral.FTC_filter.nhds_right intervalIntegral.FTCFilter.nhdsRight +-/ +#print intervalIntegral.FTCFilter.nhdsIcc /- instance nhdsIcc {x a b : ℝ} [h : Fact (x ∈ Icc a b)] : FTCFilter x (𝓝[Icc a b] x) (𝓝[Icc a b] x) where pure_le := pure_le_nhdsWithin h.out le_nhds := inf_le_left #align interval_integral.FTC_filter.nhds_Icc intervalIntegral.FTCFilter.nhdsIcc +-/ +#print intervalIntegral.FTCFilter.nhdsUIcc /- instance nhdsUIcc {x a b : ℝ} [h : Fact (x ∈ [a, b])] : FTCFilter x (𝓝[[a, b]] x) (𝓝[[a, b]] x) := haveI : Fact (x ∈ Set.Icc (min a b) (max a b)) := h FTC_filter.nhds_Icc #align interval_integral.FTC_filter.nhds_uIcc intervalIntegral.FTCFilter.nhdsUIcc +-/ end FTCFilter @@ -261,6 +277,7 @@ section variable {f : ℝ → E} {a b : ℝ} {c ca cb : E} {l l' la la' lb lb' : Filter ℝ} {lt : Filter ι} {μ : Measure ℝ} {u v ua va ub vb : ι → ℝ} +#print intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae' /- /-- Fundamental theorem of calculus-1, local version for any measure. Let filters `l` and `l'` be related by `tendsto_Ixx_class Ioc`. If `f` has a finite limit `c` at `l' ⊓ μ.ae`, where `μ` is a measure @@ -290,7 +307,9 @@ theorem measure_integral_sub_linear_isLittleO_of_tendsto_ae' [IsMeasurablyGenera abel all_goals intro t; cases' le_total (u t) (v t) with huv huv <;> simp [huv] #align interval_integral.measure_integral_sub_linear_is_o_of_tendsto_ae' intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae' +-/ +#print intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_le' /- /-- Fundamental theorem of calculus-1, local version for any measure. Let filters `l` and `l'` be related by `tendsto_Ixx_class Ioc`. If `f` has a finite limit `c` at `l ⊓ μ.ae`, where `μ` is a measure @@ -311,7 +330,9 @@ theorem measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_le' [IsMeasurably (huv.mono fun x hx => by simp [integral_const', hx]) (huv.mono fun x hx => by simp [integral_const', hx]) #align interval_integral.measure_integral_sub_linear_is_o_of_tendsto_ae_of_le' intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_le' +-/ +#print intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_ge' /- /-- Fundamental theorem of calculus-1, local version for any measure. Let filters `l` and `l'` be related by `tendsto_Ixx_class Ioc`. If `f` has a finite limit `c` at `l ⊓ μ.ae`, where `μ` is a measure @@ -332,6 +353,7 @@ theorem measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_ge' [IsMeasurably huv).neg_left.congr_left fun t => by simp [integral_symm (u t), add_comm] #align interval_integral.measure_integral_sub_linear_is_o_of_tendsto_ae_of_ge' intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_ge' +-/ section @@ -618,6 +640,7 @@ theorem integral_hasStrictFDerivAt_of_tendsto_ae (hf : IntervalIntegrable f volu · exact is_O_fst_prod.norm_left.add is_O_snd_prod.norm_left #align interval_integral.integral_has_strict_fderiv_at_of_tendsto_ae intervalIntegral.integral_hasStrictFDerivAt_of_tendsto_ae +#print intervalIntegral.integral_hasStrictFDerivAt /- /-- Fundamental theorem of calculus-1: if `f : ℝ → E` is integrable on `a..b` and `f` is continuous at `a` and `b`, then `(u, v) ↦ ∫ x in u..v, f x` has derivative `(u, v) ↦ v • cb - u • ca` at `(a, b)` in the sense of strict differentiability. -/ @@ -629,6 +652,7 @@ theorem integral_hasStrictFDerivAt (hf : IntervalIntegrable f volume a b) integral_hasStrictFDerivAt_of_tendsto_ae hf hmeas_a hmeas_b (ha.mono_left inf_le_left) (hb.mono_left inf_le_left) #align interval_integral.integral_has_strict_fderiv_at intervalIntegral.integral_hasStrictFDerivAt +-/ /-- **First Fundamental Theorem of Calculus**: if `f : ℝ → E` is integrable on `a..b` and `f x` has a finite limit `c` almost surely at `b`, then `u ↦ ∫ x in a..u, f x` has derivative `c` at `b` in @@ -640,6 +664,7 @@ theorem integral_hasStrictDerivAt_of_tendsto_ae_right (hf : IntervalIntegrable f continuousAt_fst #align interval_integral.integral_has_strict_deriv_at_of_tendsto_ae_right intervalIntegral.integral_hasStrictDerivAt_of_tendsto_ae_right +#print intervalIntegral.integral_hasStrictDerivAt_right /- /-- Fundamental theorem of calculus-1: if `f : ℝ → E` is integrable on `a..b` and `f` is continuous at `b`, then `u ↦ ∫ x in a..u, f x` has derivative `f b` at `b` in the sense of strict differentiability. -/ @@ -648,6 +673,7 @@ theorem integral_hasStrictDerivAt_right (hf : IntervalIntegrable f volume a b) HasStrictDerivAt (fun u => ∫ x in a..u, f x) (f b) b := integral_hasStrictDerivAt_of_tendsto_ae_right hf hmeas (hb.mono_left inf_le_left) #align interval_integral.integral_has_strict_deriv_at_right intervalIntegral.integral_hasStrictDerivAt_right +-/ /-- Fundamental theorem of calculus-1: if `f : ℝ → E` is integrable on `a..b` and `f x` has a finite limit `c` almost surely at `a`, then `u ↦ ∫ x in u..b, f x` has derivative `-c` at `a` in the sense @@ -668,6 +694,7 @@ theorem integral_hasStrictDerivAt_left (hf : IntervalIntegrable f volume a b) simpa only [← integral_symm] using (integral_has_strict_deriv_at_right hf.symm hmeas ha).neg #align interval_integral.integral_has_strict_deriv_at_left intervalIntegral.integral_hasStrictDerivAt_left +#print Continuous.integral_hasStrictDerivAt /- /-- Fundamental theorem of calculus-1: if `f : ℝ → E` is continuous, then `u ↦ ∫ x in a..u, f x` has derivative `f b` at `b` in the sense of strict differentiability. -/ theorem Continuous.integral_hasStrictDerivAt {f : ℝ → E} (hf : Continuous f) (a b : ℝ) : @@ -675,13 +702,16 @@ theorem Continuous.integral_hasStrictDerivAt {f : ℝ → E} (hf : Continuous f) integral_hasStrictDerivAt_right (hf.IntervalIntegrable _ _) (hf.StronglyMeasurableAtFilter _ _) hf.ContinuousAt #align continuous.integral_has_strict_deriv_at Continuous.integral_hasStrictDerivAt +-/ +#print Continuous.deriv_integral /- /-- Fundamental theorem of calculus-1: if `f : ℝ → E` is continuous, then the derivative of `u ↦ ∫ x in a..u, f x` at `b` is `f b`. -/ theorem Continuous.deriv_integral (f : ℝ → E) (hf : Continuous f) (a b : ℝ) : deriv (fun u => ∫ x : ℝ in a..u, f x) b = f b := (hf.integral_hasStrictDerivAt a b).HasDerivAt.deriv #align continuous.deriv_integral Continuous.deriv_integral +-/ /-! #### Fréchet differentiability @@ -702,6 +732,7 @@ theorem integral_hasFDerivAt_of_tendsto_ae (hf : IntervalIntegrable f volume a b (integral_hasStrictFDerivAt_of_tendsto_ae hf hmeas_a hmeas_b ha hb).HasFDerivAt #align interval_integral.integral_has_fderiv_at_of_tendsto_ae intervalIntegral.integral_hasFDerivAt_of_tendsto_ae +#print intervalIntegral.integral_hasFDerivAt /- /-- Fundamental theorem of calculus-1: if `f : ℝ → E` is integrable on `a..b` and `f` is continuous at `a` and `b`, then `(u, v) ↦ ∫ x in u..v, f x` has derivative `(u, v) ↦ v • cb - u • ca` at `(a, b)`. -/ @@ -712,6 +743,7 @@ theorem integral_hasFDerivAt (hf : IntervalIntegrable f volume a b) ((snd ℝ ℝ ℝ).smul_right (f b) - (fst ℝ ℝ ℝ).smul_right (f a)) (a, b) := (integral_hasStrictFDerivAt hf hmeas_a hmeas_b ha hb).HasFDerivAt #align interval_integral.integral_has_fderiv_at intervalIntegral.integral_hasFDerivAt +-/ /-- Fundamental theorem of calculus-1: if `f : ℝ → E` is integrable on `a..b` and `f x` has finite limits `ca` and `cb` almost surely as `x` tends to `a` and `b`, respectively, then `fderiv` @@ -743,6 +775,7 @@ theorem integral_hasDerivAt_of_tendsto_ae_right (hf : IntervalIntegrable f volum (integral_hasStrictDerivAt_of_tendsto_ae_right hf hmeas hb).HasDerivAt #align interval_integral.integral_has_deriv_at_of_tendsto_ae_right intervalIntegral.integral_hasDerivAt_of_tendsto_ae_right +#print intervalIntegral.integral_hasDerivAt_right /- /-- Fundamental theorem of calculus-1: if `f : ℝ → E` is integrable on `a..b` and `f` is continuous at `b`, then `u ↦ ∫ x in a..u, f x` has derivative `f b` at `b`. -/ theorem integral_hasDerivAt_right (hf : IntervalIntegrable f volume a b) @@ -750,6 +783,7 @@ theorem integral_hasDerivAt_right (hf : IntervalIntegrable f volume a b) HasDerivAt (fun u => ∫ x in a..u, f x) (f b) b := (integral_hasStrictDerivAt_right hf hmeas hb).HasDerivAt #align interval_integral.integral_has_deriv_at_right intervalIntegral.integral_hasDerivAt_right +-/ /-- Fundamental theorem of calculus: if `f : ℝ → E` is integrable on `a..b` and `f` has a finite limit `c` almost surely at `b`, then the derivative of `u ↦ ∫ x in a..u, f x` at `b` equals `c`. -/ @@ -759,6 +793,7 @@ theorem deriv_integral_of_tendsto_ae_right (hf : IntervalIntegrable f volume a b (integral_hasDerivAt_of_tendsto_ae_right hf hmeas hb).deriv #align interval_integral.deriv_integral_of_tendsto_ae_right intervalIntegral.deriv_integral_of_tendsto_ae_right +#print intervalIntegral.deriv_integral_right /- /-- Fundamental theorem of calculus: if `f : ℝ → E` is integrable on `a..b` and `f` is continuous at `b`, then the derivative of `u ↦ ∫ x in a..u, f x` at `b` equals `f b`. -/ theorem deriv_integral_right (hf : IntervalIntegrable f volume a b) @@ -766,6 +801,7 @@ theorem deriv_integral_right (hf : IntervalIntegrable f volume a b) deriv (fun u => ∫ x in a..u, f x) b = f b := (integral_hasDerivAt_right hf hmeas hb).deriv #align interval_integral.deriv_integral_right intervalIntegral.deriv_integral_right +-/ /-- Fundamental theorem of calculus-1: if `f : ℝ → E` is integrable on `a..b` and `f x` has a finite limit `c` almost surely at `a`, then `u ↦ ∫ x in u..b, f x` has derivative `-c` at `a`. -/ @@ -835,6 +871,7 @@ theorem integral_hasFDerivWithinAt_of_tendsto_ae (hf : IntervalIntegrable f volu #align interval_integral.integral_has_fderiv_within_at_of_tendsto_ae intervalIntegral.integral_hasFDerivWithinAt_of_tendsto_ae /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ +#print intervalIntegral.integral_hasFDerivWithinAt /- /-- Let `f` be a measurable function integrable on `a..b`. The function `(u, v) ↦ ∫ x in u..v, f x` has derivative `(u, v) ↦ v • f b - u • f a` within `s × t` at `(a, b)`, where `s ∈ {Iic a, {a}, Ici a, univ}` and `t ∈ {Iic b, {b}, Ici b, univ}` provided that `f` tends to @@ -857,6 +894,7 @@ theorem integral_hasFDerivWithinAt (hf : IntervalIntegrable f volume a b) integral_hasFDerivWithinAt_of_tendsto_ae hf hmeas_a hmeas_b (ha.mono_left inf_le_left) (hb.mono_left inf_le_left) #align interval_integral.integral_has_fderiv_within_at intervalIntegral.integral_hasFDerivWithinAt +-/ /- ./././Mathport/Syntax/Translate/Expr.lean:330:4: warning: unsupported (TODO): `[tacs] -/ /-- An auxiliary tactic closing goals `unique_diff_within_at ℝ s a` where @@ -900,6 +938,7 @@ theorem integral_hasDerivWithinAt_of_tendsto_ae_right (hf : IntervalIntegrable f (tendsto_const_pure.mono_right FTCFilter.pure_le) tendsto_id #align interval_integral.integral_has_deriv_within_at_of_tendsto_ae_right intervalIntegral.integral_hasDerivWithinAt_of_tendsto_ae_right +#print intervalIntegral.integral_hasDerivWithinAt_right /- /-- Fundamental theorem of calculus: if `f : ℝ → E` is integrable on `a..b` and `f x` is continuous from the left or from the right at `b`, then `u ↦ ∫ x in a..u, f x` has left (resp., right) derivative `f b` at `b`. -/ @@ -908,6 +947,7 @@ theorem integral_hasDerivWithinAt_right (hf : IntervalIntegrable f volume a b) { (hb : ContinuousWithinAt f t b) : HasDerivWithinAt (fun u => ∫ x in a..u, f x) (f b) s b := integral_hasDerivWithinAt_of_tendsto_ae_right hf hmeas (hb.mono_left inf_le_left) #align interval_integral.integral_has_deriv_within_at_right intervalIntegral.integral_hasDerivWithinAt_right +-/ /-- Fundamental theorem of calculus: if `f : ℝ → E` is integrable on `a..b` and `f x` has a finite limit `c` almost surely as `x` tends to `b` from the right or from the left, then the right @@ -920,6 +960,7 @@ theorem derivWithin_integral_of_tendsto_ae_right (hf : IntervalIntegrable f volu (integral_hasDerivWithinAt_of_tendsto_ae_right hf hmeas hb).derivWithin hs #align interval_integral.deriv_within_integral_of_tendsto_ae_right intervalIntegral.derivWithin_integral_of_tendsto_ae_right +#print intervalIntegral.derivWithin_integral_right /- /-- Fundamental theorem of calculus: if `f : ℝ → E` is integrable on `a..b` and `f x` is continuous on the right or on the left at `b`, then the right (resp., left) derivative of `u ↦ ∫ x in a..u, f x` at `b` equals `f b`. -/ @@ -930,6 +971,7 @@ theorem derivWithin_integral_right (hf : IntervalIntegrable f volume a b) {s t : derivWithin (fun u => ∫ x in a..u, f x) s b = f b := (integral_hasDerivWithinAt_right hf hmeas hb).derivWithin hs #align interval_integral.deriv_within_integral_right intervalIntegral.derivWithin_integral_right +-/ /-- Fundamental theorem of calculus: if `f : ℝ → E` is integrable on `a..b` and `f x` has a finite limit `c` almost surely as `x` tends to `a` from the right or from the left, @@ -974,6 +1016,7 @@ theorem derivWithin_integral_left (hf : IntervalIntegrable f volume a b) {s t : (integral_hasDerivWithinAt_left hf hmeas ha).derivWithin hs #align interval_integral.deriv_within_integral_left intervalIntegral.derivWithin_integral_left +#print intervalIntegral.differentiableOn_integral_of_continuous /- /-- The integral of a continuous function is differentiable on a real set `s`. -/ theorem differentiableOn_integral_of_continuous {s : Set ℝ} (hintg : ∀ x ∈ s, IntervalIntegrable f volume a x) (hcont : Continuous f) : @@ -981,6 +1024,7 @@ theorem differentiableOn_integral_of_continuous {s : Set ℝ} (integral_hasDerivAt_right (hintg y hy) hcont.AEStronglyMeasurable.StronglyMeasurableAtFilter hcont.ContinuousAt).DifferentiableAt.DifferentiableWithinAt #align interval_integral.differentiable_on_integral_of_continuous intervalIntegral.differentiableOn_integral_of_continuous +-/ /-! ### Fundamental theorem of calculus, part 2 @@ -1012,10 +1056,9 @@ Auxiliary lemma in the proof of `integral_eq_sub_of_has_deriv_right_of_le`. We give the slightly more general version that `g b - g a ≤ ∫ y in a..b, φ y` when `g' ≤ φ` and `φ` is integrable (even if `g'` is not known to be integrable). Version assuming that `g` is differentiable on `[a, b)`. -/ -theorem sub_le_integral_of_has_deriv_right_of_le_Ico (hab : a ≤ b) - (hcont : ContinuousOn g (Icc a b)) (hderiv : ∀ x ∈ Ico a b, HasDerivWithinAt g (g' x) (Ioi x) x) - (φint : IntegrableOn φ (Icc a b)) (hφg : ∀ x ∈ Ico a b, g' x ≤ φ x) : - g b - g a ≤ ∫ y in a..b, φ y := +theorem sub_le_integral_of_hasDeriv_right_of_le_Ico (hab : a ≤ b) (hcont : ContinuousOn g (Icc a b)) + (hderiv : ∀ x ∈ Ico a b, HasDerivWithinAt g (g' x) (Ioi x) x) (φint : IntegrableOn φ (Icc a b)) + (hφg : ∀ x ∈ Ico a b, g' x ≤ φ x) : g b - g a ≤ ∫ y in a..b, φ y := by refine' le_of_forall_pos_le_add fun ε εpos => _ -- Bound from above `g'` by a lower-semicontinuous function `G'`. @@ -1120,7 +1163,7 @@ theorem sub_le_integral_of_has_deriv_right_of_le_Ico (hab : a ≤ b) · rw [intervalIntegral.integral_of_le hab] simp only [integral_Icc_eq_integral_Ioc', Real.volume_singleton] -#align interval_integral.sub_le_integral_of_has_deriv_right_of_le_Ico intervalIntegral.sub_le_integral_of_has_deriv_right_of_le_Ico +#align interval_integral.sub_le_integral_of_has_deriv_right_of_le_Ico intervalIntegral.sub_le_integral_of_hasDeriv_right_of_le_Ico /-- Hard part of FTC-2 for integrable derivatives, real-valued functions: one has `g b - g a ≤ ∫ y in a..b, g' y` when `g'` is integrable. @@ -1128,7 +1171,7 @@ Auxiliary lemma in the proof of `integral_eq_sub_of_has_deriv_right_of_le`. We give the slightly more general version that `g b - g a ≤ ∫ y in a..b, φ y` when `g' ≤ φ` and `φ` is integrable (even if `g'` is not known to be integrable). Version assuming that `g` is differentiable on `(a, b)`. -/ -theorem sub_le_integral_of_has_deriv_right_of_le (hab : a ≤ b) (hcont : ContinuousOn g (Icc a b)) +theorem sub_le_integral_of_hasDeriv_right_of_le (hab : a ≤ b) (hcont : ContinuousOn g (Icc a b)) (hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x) (φint : IntegrableOn φ (Icc a b)) (hφg : ∀ x ∈ Ioo a b, g' x ≤ φ x) : g b - g a ≤ ∫ y in a..b, φ y := by @@ -1156,10 +1199,10 @@ theorem sub_le_integral_of_has_deriv_right_of_le (hab : a ≤ b) (hcont : Contin (φint.mono_set (Icc_subset_Icc ht.1.le le_rfl)) fun x hx => hφg x ⟨ht.1.trans_le hx.1, hx.2⟩ rw [closure_Ioc a_lt_b.ne] at A exact (A (left_mem_Icc.2 hab)).1 -#align interval_integral.sub_le_integral_of_has_deriv_right_of_le intervalIntegral.sub_le_integral_of_has_deriv_right_of_le +#align interval_integral.sub_le_integral_of_has_deriv_right_of_le intervalIntegral.sub_le_integral_of_hasDeriv_right_of_le /-- Auxiliary lemma in the proof of `integral_eq_sub_of_has_deriv_right_of_le`. -/ -theorem integral_le_sub_of_has_deriv_right_of_le (hab : a ≤ b) (hcont : ContinuousOn g (Icc a b)) +theorem integral_le_sub_of_hasDeriv_right_of_le (hab : a ≤ b) (hcont : ContinuousOn g (Icc a b)) (hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x) (φint : IntegrableOn φ (Icc a b)) (hφg : ∀ x ∈ Ioo a b, φ x ≤ g' x) : (∫ y in a..b, φ y) ≤ g b - g a := by @@ -1169,22 +1212,22 @@ theorem integral_le_sub_of_has_deriv_right_of_le (hab : a ≤ b) (hcont : Contin fun x hx => neg_le_neg (hφg x hx) · abel · simp only [← integral_neg]; rfl -#align interval_integral.integral_le_sub_of_has_deriv_right_of_le intervalIntegral.integral_le_sub_of_has_deriv_right_of_le +#align interval_integral.integral_le_sub_of_has_deriv_right_of_le intervalIntegral.integral_le_sub_of_hasDeriv_right_of_le /-- Auxiliary lemma in the proof of `integral_eq_sub_of_has_deriv_right_of_le`: real version -/ -theorem integral_eq_sub_of_has_deriv_right_of_le_real (hab : a ≤ b) +theorem integral_eq_sub_of_hasDeriv_right_of_le_real (hab : a ≤ b) (hcont : ContinuousOn g (Icc a b)) (hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x) (g'int : IntegrableOn g' (Icc a b)) : (∫ y in a..b, g' y) = g b - g a := - le_antisymm (integral_le_sub_of_has_deriv_right_of_le hab hcont hderiv g'int fun x hx => le_rfl) - (sub_le_integral_of_has_deriv_right_of_le hab hcont hderiv g'int fun x hx => le_rfl) -#align interval_integral.integral_eq_sub_of_has_deriv_right_of_le_real intervalIntegral.integral_eq_sub_of_has_deriv_right_of_le_real + le_antisymm (integral_le_sub_of_hasDeriv_right_of_le hab hcont hderiv g'int fun x hx => le_rfl) + (sub_le_integral_of_hasDeriv_right_of_le hab hcont hderiv g'int fun x hx => le_rfl) +#align interval_integral.integral_eq_sub_of_has_deriv_right_of_le_real intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le_real variable {f' : ℝ → E} /-- **Fundamental theorem of calculus-2**: If `f : ℝ → E` is continuous on `[a, b]` (where `a ≤ b`) and has a right derivative at `f' x` for all `x` in `(a, b)`, and `f'` is integrable on `[a, b]`, then `∫ y in a..b, f' y` equals `f b - f a`. -/ -theorem integral_eq_sub_of_has_deriv_right_of_le (hab : a ≤ b) (hcont : ContinuousOn f (Icc a b)) +theorem integral_eq_sub_of_hasDeriv_right_of_le (hab : a ≤ b) (hcont : ContinuousOn f (Icc a b)) (hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt f (f' x) (Ioi x) x) (f'int : IntervalIntegrable f' volume a b) : (∫ y in a..b, f' y) = f b - f a := by @@ -1194,12 +1237,12 @@ theorem integral_eq_sub_of_has_deriv_right_of_le (hab : a ≤ b) (hcont : Contin integral_eq_sub_of_has_deriv_right_of_le_real hab (g.continuous.comp_continuous_on hcont) (fun x hx => g.has_fderiv_at.comp_has_deriv_within_at x (hderiv x hx)) (g.integrable_comp ((intervalIntegrable_iff_integrable_Icc_of_le hab).1 f'int)) -#align interval_integral.integral_eq_sub_of_has_deriv_right_of_le intervalIntegral.integral_eq_sub_of_has_deriv_right_of_le +#align interval_integral.integral_eq_sub_of_has_deriv_right_of_le intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le /-- Fundamental theorem of calculus-2: If `f : ℝ → E` is continuous on `[a, b]` and has a right derivative at `f' x` for all `x` in `[a, b)`, and `f'` is integrable on `[a, b]` then `∫ y in a..b, f' y` equals `f b - f a`. -/ -theorem integral_eq_sub_of_has_deriv_right (hcont : ContinuousOn f (uIcc a b)) +theorem integral_eq_sub_of_hasDeriv_right (hcont : ContinuousOn f (uIcc a b)) (hderiv : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x) (hint : IntervalIntegrable f' volume a b) : (∫ y in a..b, f' y) = f b - f a := by @@ -1208,7 +1251,7 @@ theorem integral_eq_sub_of_has_deriv_right (hcont : ContinuousOn f (uIcc a b)) apply integral_eq_sub_of_has_deriv_right_of_le hab hcont hderiv hint · simp only [uIcc_of_ge, min_eq_right, max_eq_left, hab] at hcont hderiv rw [integral_symm, integral_eq_sub_of_has_deriv_right_of_le hab hcont hderiv hint.symm, neg_sub] -#align interval_integral.integral_eq_sub_of_has_deriv_right intervalIntegral.integral_eq_sub_of_has_deriv_right +#align interval_integral.integral_eq_sub_of_has_deriv_right intervalIntegral.integral_eq_sub_of_hasDeriv_right /-- Fundamental theorem of calculus-2: If `f : ℝ → E` is continuous on `[a, b]` (where `a ≤ b`) and has a derivative at `f' x` for all `x` in `(a, b)`, and `f'` is integrable on `[a, b]`, then @@ -1216,7 +1259,7 @@ theorem integral_eq_sub_of_has_deriv_right (hcont : ContinuousOn f (uIcc a b)) theorem integral_eq_sub_of_hasDerivAt_of_le (hab : a ≤ b) (hcont : ContinuousOn f (Icc a b)) (hderiv : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x) (hint : IntervalIntegrable f' volume a b) : (∫ y in a..b, f' y) = f b - f a := - integral_eq_sub_of_has_deriv_right_of_le hab hcont (fun x hx => (hderiv x hx).HasDerivWithinAt) + integral_eq_sub_of_hasDeriv_right_of_le hab hcont (fun x hx => (hderiv x hx).HasDerivWithinAt) hint #align interval_integral.integral_eq_sub_of_has_deriv_at_of_le intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le @@ -1224,7 +1267,7 @@ theorem integral_eq_sub_of_hasDerivAt_of_le (hab : a ≤ b) (hcont : ContinuousO `[a, b]` and `f'` is integrable on `[a, b]`, then `∫ y in a..b, f' y` equals `f b - f a`. -/ theorem integral_eq_sub_of_hasDerivAt (hderiv : ∀ x ∈ uIcc a b, HasDerivAt f (f' x) x) (hint : IntervalIntegrable f' volume a b) : (∫ y in a..b, f' y) = f b - f a := - integral_eq_sub_of_has_deriv_right (HasDerivAt.continuousOn hderiv) + integral_eq_sub_of_hasDeriv_right (HasDerivAt.continuousOn hderiv) (fun x hx => (hderiv _ (mem_Icc_of_Ioo hx)).HasDerivWithinAt) hint #align interval_integral.integral_eq_sub_of_has_deriv_at intervalIntegral.integral_eq_sub_of_hasDerivAt @@ -1439,6 +1482,7 @@ theorem integral_comp_smul_deriv'' {f f' : ℝ → ℝ} {g : ℝ → E} (hf : Co exact hg.integrable_on_Icc #align interval_integral.integral_comp_smul_deriv'' intervalIntegral.integral_comp_smul_deriv'' +#print intervalIntegral.integral_comp_smul_deriv' /- /-- Change of variables. If `f` is has continuous derivative `f'` on `[a, b]`, and `g` is continuous on `f '' [a, b]`, then we can substitute `u = f x` to get `∫ x in a..b, f' x • (g ∘ f) x = ∫ u in f a..f b, g u`. @@ -1451,7 +1495,9 @@ theorem integral_comp_smul_deriv' {f f' : ℝ → ℝ} {g : ℝ → E} integral_comp_smul_deriv'' (fun x hx => (h x hx).ContinuousAt.ContinuousWithinAt) (fun x hx => (h x <| Ioo_subset_Icc_self hx).HasDerivWithinAt) h' hg #align interval_integral.integral_comp_smul_deriv' intervalIntegral.integral_comp_smul_deriv' +-/ +#print intervalIntegral.integral_comp_smul_deriv /- /-- Change of variables, most common version. If `f` is has continuous derivative `f'` on `[a, b]`, and `g` is continuous, then we can substitute `u = f x` to get `∫ x in a..b, f' x • (g ∘ f) x = ∫ u in f a..f b, g u`. @@ -1461,6 +1507,7 @@ theorem integral_comp_smul_deriv {f f' : ℝ → ℝ} {g : ℝ → E} (hg : Continuous g) : (∫ x in a..b, f' x • (g ∘ f) x) = ∫ x in f a..f b, g x := integral_comp_smul_deriv' h h' hg.ContinuousOn #align interval_integral.integral_comp_smul_deriv intervalIntegral.integral_comp_smul_deriv +-/ theorem integral_deriv_comp_smul_deriv' {f f' : ℝ → ℝ} {g g' : ℝ → E} (hf : ContinuousOn f [a, b]) (hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x) diff --git a/Mathbin/MeasureTheory/Integral/IntervalAverage.lean b/Mathbin/MeasureTheory/Integral/IntervalAverage.lean index 92a20077cf..15f5baa702 100644 --- a/Mathbin/MeasureTheory/Integral/IntervalAverage.lean +++ b/Mathbin/MeasureTheory/Integral/IntervalAverage.lean @@ -39,9 +39,11 @@ variable {E : Type _} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace -- mathport name: «expr⨍ in .. , » notation3"⨍ "(...)" in "a".."b", "r:(scoped f => average Measure.restrict volume Ι a b f) => r +#print interval_average_symm /- theorem interval_average_symm (f : ℝ → E) (a b : ℝ) : (⨍ x in a..b, f x) = ⨍ x in b..a, f x := by rw [set_average_eq, set_average_eq, uIoc_swap] #align interval_average_symm interval_average_symm +-/ theorem interval_average_eq (f : ℝ → E) (a b : ℝ) : (⨍ x in a..b, f x) = (b - a)⁻¹ • ∫ x in a..b, f x := diff --git a/Mathbin/RingTheory/ClassGroup.lean b/Mathbin/RingTheory/ClassGroup.lean index c7a69fb4f4..840be175c4 100644 --- a/Mathbin/RingTheory/ClassGroup.lean +++ b/Mathbin/RingTheory/ClassGroup.lean @@ -95,12 +95,14 @@ end variable (R) [IsDomain R] +#print ClassGroup /- /-- The ideal class group of `R` is the group of invertible fractional ideals modulo the principal ideals. -/ def ClassGroup := (FractionalIdeal R⁰ (FractionRing R))ˣ ⧸ (toPrincipalIdeal R (FractionRing R)).range deriving CommGroup #align class_group ClassGroup +-/ noncomputable instance : Inhabited (ClassGroup R) := ⟨1⟩ @@ -394,6 +396,7 @@ noncomputable instance [IsPrincipalIdealRing R] : Fintype (ClassGroup R) rw [Finset.mem_singleton] exact class_group.mk_eq_one_iff.mpr (I : FractionalIdeal R⁰ (FractionRing R)).IsPrincipal +#print card_classGroup_eq_one /- /-- The class number of a principal ideal domain is `1`. -/ theorem card_classGroup_eq_one [IsPrincipalIdealRing R] : Fintype.card (ClassGroup R) = 1 := by @@ -402,7 +405,9 @@ theorem card_classGroup_eq_one [IsPrincipalIdealRing R] : Fintype.card (ClassGro refine' ClassGroup.induction (FractionRing R) fun I => _ exact class_group.mk_eq_one_iff.mpr (I : FractionalIdeal R⁰ (FractionRing R)).IsPrincipal #align card_class_group_eq_one card_classGroup_eq_one +-/ +#print card_classGroup_eq_one_iff /- /-- The class number is `1` iff the ring of integers is a principal ideal domain. -/ theorem card_classGroup_eq_one_iff [IsDedekindDomain R] [Fintype (ClassGroup R)] : Fintype.card (ClassGroup R) = 1 ↔ IsPrincipalIdealRing R := @@ -416,4 +421,5 @@ theorem card_classGroup_eq_one_iff [IsDedekindDomain R] [Fintype (ClassGroup R)] · rw [hI]; exact bot_isPrincipal exact (ClassGroup.mk0_eq_one_iff (mem_non_zero_divisors_iff_ne_zero.mpr hI)).mp (eq_one _) #align card_class_group_eq_one_iff card_classGroup_eq_one_iff +-/ diff --git a/Mathbin/RingTheory/Polynomial/Cyclotomic/Basic.lean b/Mathbin/RingTheory/Polynomial/Cyclotomic/Basic.lean index b19ae5797c..cc5a6ab904 100644 --- a/Mathbin/RingTheory/Polynomial/Cyclotomic/Basic.lean +++ b/Mathbin/RingTheory/Polynomial/Cyclotomic/Basic.lean @@ -69,24 +69,30 @@ section IsDomain variable {R : Type _} [CommRing R] [IsDomain R] +#print Polynomial.cyclotomic' /- /-- The modified `n`-th cyclotomic polynomial with coefficients in `R`, it is the usual cyclotomic polynomial if there is a primitive `n`-th root of unity in `R`. -/ def cyclotomic' (n : ℕ) (R : Type _) [CommRing R] [IsDomain R] : R[X] := ∏ μ in primitiveRoots n R, X - C μ #align polynomial.cyclotomic' Polynomial.cyclotomic' +-/ +#print Polynomial.cyclotomic'_zero /- /-- The zeroth modified cyclotomic polyomial is `1`. -/ @[simp] theorem cyclotomic'_zero (R : Type _) [CommRing R] [IsDomain R] : cyclotomic' 0 R = 1 := by simp only [cyclotomic', Finset.prod_empty, primitiveRoots_zero] #align polynomial.cyclotomic'_zero Polynomial.cyclotomic'_zero +-/ +#print Polynomial.cyclotomic'_one /- /-- The first modified cyclotomic polyomial is `X - 1`. -/ @[simp] theorem cyclotomic'_one (R : Type _) [CommRing R] [IsDomain R] : cyclotomic' 1 R = X - 1 := by simp only [cyclotomic', Finset.prod_singleton, RingHom.map_one, IsPrimitiveRoot.primitiveRoots_one] #align polynomial.cyclotomic'_one Polynomial.cyclotomic'_one +-/ /-- The second modified cyclotomic polyomial is `X + 1` if the characteristic of `R` is not `2`. -/ @[simp] @@ -100,17 +106,22 @@ theorem cyclotomic'_two (R : Type _) [CommRing R] [IsDomain R] (p : ℕ) [CharP simp only [prim_root_two, Finset.prod_singleton, RingHom.map_neg, RingHom.map_one, sub_neg_eq_add] #align polynomial.cyclotomic'_two Polynomial.cyclotomic'_two +#print Polynomial.cyclotomic'.monic /- /-- `cyclotomic' n R` is monic. -/ theorem cyclotomic'.monic (n : ℕ) (R : Type _) [CommRing R] [IsDomain R] : (cyclotomic' n R).Monic := monic_prod_of_monic _ _ fun z hz => monic_X_sub_C _ #align polynomial.cyclotomic'.monic Polynomial.cyclotomic'.monic +-/ +#print Polynomial.cyclotomic'_ne_zero /- /-- `cyclotomic' n R` is different from `0`. -/ theorem cyclotomic'_ne_zero (n : ℕ) (R : Type _) [CommRing R] [IsDomain R] : cyclotomic' n R ≠ 0 := (cyclotomic'.monic n R).NeZero #align polynomial.cyclotomic'_ne_zero Polynomial.cyclotomic'_ne_zero +-/ +#print Polynomial.natDegree_cyclotomic' /- /-- The natural degree of `cyclotomic' n R` is `totient n` if there is a primitive root of unity in `R`. -/ theorem natDegree_cyclotomic' {ζ : R} {n : ℕ} (h : IsPrimitiveRoot ζ n) : @@ -123,22 +134,27 @@ theorem natDegree_cyclotomic' {ζ : R} {n : ℕ} (h : IsPrimitiveRoot ζ n) : intro z hz exact X_sub_C_ne_zero z #align polynomial.nat_degree_cyclotomic' Polynomial.natDegree_cyclotomic' +-/ +#print Polynomial.degree_cyclotomic' /- /-- The degree of `cyclotomic' n R` is `totient n` if there is a primitive root of unity in `R`. -/ theorem degree_cyclotomic' {ζ : R} {n : ℕ} (h : IsPrimitiveRoot ζ n) : (cyclotomic' n R).degree = Nat.totient n := by simp only [degree_eq_nat_degree (cyclotomic'_ne_zero n R), nat_degree_cyclotomic' h] #align polynomial.degree_cyclotomic' Polynomial.degree_cyclotomic' +-/ +#print Polynomial.roots_of_cyclotomic /- /-- The roots of `cyclotomic' n R` are the primitive `n`-th roots of unity. -/ theorem roots_of_cyclotomic (n : ℕ) (R : Type _) [CommRing R] [IsDomain R] : (cyclotomic' n R).roots = (primitiveRoots n R).val := by rw [cyclotomic']; exact roots_prod_X_sub_C (primitiveRoots n R) #align polynomial.roots_of_cyclotomic Polynomial.roots_of_cyclotomic +-/ /-- If there is a primitive `n`th root of unity in `K`, then `X ^ n - 1 = ∏ (X - μ)`, where `μ` varies over the `n`-th roots of unity. -/ -theorem x_pow_sub_one_eq_prod {ζ : R} {n : ℕ} (hpos : 0 < n) (h : IsPrimitiveRoot ζ n) : +theorem X_pow_sub_one_eq_prod {ζ : R} {n : ℕ} (hpos : 0 < n) (h : IsPrimitiveRoot ζ n) : X ^ n - 1 = ∏ ζ in nthRootsFinset n R, X - C ζ := by rw [nth_roots_finset, ← Multiset.toFinset_eq (IsPrimitiveRoot.nthRoots_nodup h)] @@ -149,7 +165,7 @@ theorem x_pow_sub_one_eq_prod {ζ : R} {n : ℕ} (hpos : 0 < n) (h : IsPrimitive apply prod_multiset_X_sub_C_of_monic_of_roots_card_eq hmonic rw [@nat_degree_X_pow_sub_C R _ _ n 1, ← nth_roots] exact IsPrimitiveRoot.card_nthRoots h -#align polynomial.X_pow_sub_one_eq_prod Polynomial.x_pow_sub_one_eq_prod +#align polynomial.X_pow_sub_one_eq_prod Polynomial.X_pow_sub_one_eq_prod end IsDomain @@ -157,6 +173,7 @@ section Field variable {K : Type _} [Field K] +#print Polynomial.cyclotomic'_splits /- /-- `cyclotomic' n K` splits. -/ theorem cyclotomic'_splits (n : ℕ) : Splits (RingHom.id K) (cyclotomic' n K) := by @@ -164,16 +181,17 @@ theorem cyclotomic'_splits (n : ℕ) : Splits (RingHom.id K) (cyclotomic' n K) : intro z hz simp only [splits_X_sub_C (RingHom.id K)] #align polynomial.cyclotomic'_splits Polynomial.cyclotomic'_splits +-/ /-- If there is a primitive `n`-th root of unity in `K`, then `X ^ n - 1`splits. -/ -theorem x_pow_sub_one_splits {ζ : K} {n : ℕ} (h : IsPrimitiveRoot ζ n) : +theorem X_pow_sub_one_splits {ζ : K} {n : ℕ} (h : IsPrimitiveRoot ζ n) : Splits (RingHom.id K) (X ^ n - C (1 : K)) := by rw [splits_iff_card_roots, ← nth_roots, IsPrimitiveRoot.card_nthRoots h, nat_degree_X_pow_sub_C] -#align polynomial.X_pow_sub_one_splits Polynomial.x_pow_sub_one_splits +#align polynomial.X_pow_sub_one_splits Polynomial.X_pow_sub_one_splits /-- If there is a primitive `n`-th root of unity in `K`, then `∏ i in nat.divisors n, cyclotomic' i K = X ^ n - 1`. -/ -theorem prod_cyclotomic'_eq_x_pow_sub_one {K : Type _} [CommRing K] [IsDomain K] {ζ : K} {n : ℕ} +theorem prod_cyclotomic'_eq_X_pow_sub_one {K : Type _} [CommRing K] [IsDomain K] {ζ : K} {n : ℕ} (hpos : 0 < n) (h : IsPrimitiveRoot ζ n) : (∏ i in Nat.divisors n, cyclotomic' i K) = X ^ n - 1 := by @@ -181,11 +199,11 @@ theorem prod_cyclotomic'_eq_x_pow_sub_one {K : Type _} [CommRing K] [IsDomain K] fun x hx y hy hne => IsPrimitiveRoot.disjoint hne simp only [X_pow_sub_one_eq_prod hpos h, cyclotomic', ← Finset.prod_biUnion hd, h.nth_roots_one_eq_bUnion_primitive_roots] -#align polynomial.prod_cyclotomic'_eq_X_pow_sub_one Polynomial.prod_cyclotomic'_eq_x_pow_sub_one +#align polynomial.prod_cyclotomic'_eq_X_pow_sub_one Polynomial.prod_cyclotomic'_eq_X_pow_sub_one /-- If there is a primitive `n`-th root of unity in `K`, then `cyclotomic' n K = (X ^ k - 1) /ₘ (∏ i in nat.proper_divisors k, cyclotomic' i K)`. -/ -theorem cyclotomic'_eq_x_pow_sub_one_div {K : Type _} [CommRing K] [IsDomain K] {ζ : K} {n : ℕ} +theorem cyclotomic'_eq_X_pow_sub_one_div {K : Type _} [CommRing K] [IsDomain K] {ζ : K} {n : ℕ} (hpos : 0 < n) (h : IsPrimitiveRoot ζ n) : cyclotomic' n K = (X ^ n - 1) /ₘ ∏ i in Nat.properDivisors n, cyclotomic' i K := by @@ -202,7 +220,7 @@ theorem cyclotomic'_eq_x_pow_sub_one_div {K : Type _} [CommRing K] [IsDomain K] rw [bot_lt_iff_ne_bot] intro h exact monic.ne_zero prod_monic (degree_eq_bot.1 h) -#align polynomial.cyclotomic'_eq_X_pow_sub_one_div Polynomial.cyclotomic'_eq_x_pow_sub_one_div +#align polynomial.cyclotomic'_eq_X_pow_sub_one_div Polynomial.cyclotomic'_eq_X_pow_sub_one_div /-- If there is a primitive `n`-th root of unity in `K`, then `cyclotomic' n K` comes from a monic polynomial with integer coefficients. -/ @@ -263,11 +281,13 @@ end Cyclotomic' section Cyclotomic +#print Polynomial.cyclotomic /- /-- The `n`-th cyclotomic polynomial with coefficients in `R`. -/ def cyclotomic (n : ℕ) (R : Type _) [Ring R] : R[X] := if h : n = 0 then 1 else map (Int.castRingHom R) (int_coeff_of_cyclotomic' (Complex.isPrimitiveRoot_exp n h)).some #align polynomial.cyclotomic Polynomial.cyclotomic +-/ theorem int_cyclotomic_rw {n : ℕ} (h : n ≠ 0) : cyclotomic n ℤ = (int_coeff_of_cyclotomic' (Complex.isPrimitiveRoot_exp n h)).some := @@ -319,12 +339,15 @@ theorem cyclotomic.eval_apply {R S : Type _} (q : R) (n : ℕ) [Ring R] [Ring S] rw [← map_cyclotomic n f, eval_map, eval₂_at_apply] #align polynomial.cyclotomic.eval_apply Polynomial.cyclotomic.eval_apply +#print Polynomial.cyclotomic_zero /- /-- The zeroth cyclotomic polyomial is `1`. -/ @[simp] theorem cyclotomic_zero (R : Type _) [Ring R] : cyclotomic 0 R = 1 := by simp only [cyclotomic, dif_pos] #align polynomial.cyclotomic_zero Polynomial.cyclotomic_zero +-/ +#print Polynomial.cyclotomic_one /- /-- The first cyclotomic polyomial is `X - 1`. -/ @[simp] theorem cyclotomic_one (R : Type _) [Ring R] : cyclotomic 1 R = X - 1 := @@ -335,24 +358,32 @@ theorem cyclotomic_one (R : Type _) [Ring R] : cyclotomic 1 R = X - 1 := rw [← map_cyclotomic_int, ← int_cyclotomic_unique hspec] simp only [map_X, Polynomial.map_one, Polynomial.map_sub] #align polynomial.cyclotomic_one Polynomial.cyclotomic_one +-/ +#print Polynomial.cyclotomic.monic /- /-- `cyclotomic n` is monic. -/ theorem cyclotomic.monic (n : ℕ) (R : Type _) [Ring R] : (cyclotomic n R).Monic := by rw [← map_cyclotomic_int] exact (int_cyclotomic_spec n).2.2.map _ #align polynomial.cyclotomic.monic Polynomial.cyclotomic.monic +-/ +#print Polynomial.cyclotomic.isPrimitive /- /-- `cyclotomic n` is primitive. -/ theorem cyclotomic.isPrimitive (n : ℕ) (R : Type _) [CommRing R] : (cyclotomic n R).IsPrimitive := (cyclotomic.monic n R).IsPrimitive #align polynomial.cyclotomic.is_primitive Polynomial.cyclotomic.isPrimitive +-/ +#print Polynomial.cyclotomic_ne_zero /- /-- `cyclotomic n R` is different from `0`. -/ theorem cyclotomic_ne_zero (n : ℕ) (R : Type _) [Ring R] [Nontrivial R] : cyclotomic n R ≠ 0 := (cyclotomic.monic n R).NeZero #align polynomial.cyclotomic_ne_zero Polynomial.cyclotomic_ne_zero +-/ +#print Polynomial.degree_cyclotomic /- /-- The degree of `cyclotomic n` is `totient n`. -/ theorem degree_cyclotomic (n : ℕ) (R : Type _) [Ring R] [Nontrivial R] : (cyclotomic n R).degree = Nat.totient n := @@ -366,23 +397,28 @@ theorem degree_cyclotomic (n : ℕ) (R : Type _) [Ring R] [Nontrivial R] : simp only [(int_cyclotomic_spec n).right.right, eq_intCast, monic.leading_coeff, Int.cast_one, Ne.def, not_false_iff, one_ne_zero] #align polynomial.degree_cyclotomic Polynomial.degree_cyclotomic +-/ +#print Polynomial.natDegree_cyclotomic /- /-- The natural degree of `cyclotomic n` is `totient n`. -/ theorem natDegree_cyclotomic (n : ℕ) (R : Type _) [Ring R] [Nontrivial R] : (cyclotomic n R).natDegree = Nat.totient n := by rw [nat_degree, degree_cyclotomic, WithBot.unbot'_coe] #align polynomial.nat_degree_cyclotomic Polynomial.natDegree_cyclotomic +-/ +#print Polynomial.degree_cyclotomic_pos /- /-- The degree of `cyclotomic n R` is positive. -/ theorem degree_cyclotomic_pos (n : ℕ) (R : Type _) (hpos : 0 < n) [Ring R] [Nontrivial R] : 0 < (cyclotomic n R).degree := by rw [degree_cyclotomic n R]; exact_mod_cast Nat.totient_pos hpos #align polynomial.degree_cyclotomic_pos Polynomial.degree_cyclotomic_pos +-/ open Finset /-- `∏ i in nat.divisors n, cyclotomic i R = X ^ n - 1`. -/ -theorem prod_cyclotomic_eq_x_pow_sub_one {n : ℕ} (hpos : 0 < n) (R : Type _) [CommRing R] : +theorem prod_cyclotomic_eq_X_pow_sub_one {n : ℕ} (hpos : 0 < n) (R : Type _) [CommRing R] : (∏ i in Nat.divisors n, cyclotomic i R) = X ^ n - 1 := by have integer : (∏ i in Nat.divisors n, cyclotomic i ℤ) = X ^ n - 1 := @@ -393,9 +429,9 @@ theorem prod_cyclotomic_eq_x_pow_sub_one {n : ℕ} (hpos : 0 < n) (R : Type _) [ exact prod_cyclotomic'_eq_X_pow_sub_one hpos (Complex.isPrimitiveRoot_exp n hpos.ne') simpa only [Polynomial.map_prod, map_cyclotomic_int, Polynomial.map_sub, Polynomial.map_one, Polynomial.map_pow, Polynomial.map_X] using congr_arg (map (Int.castRingHom R)) integer -#align polynomial.prod_cyclotomic_eq_X_pow_sub_one Polynomial.prod_cyclotomic_eq_x_pow_sub_one +#align polynomial.prod_cyclotomic_eq_X_pow_sub_one Polynomial.prod_cyclotomic_eq_X_pow_sub_one -theorem cyclotomic.dvd_x_pow_sub_one (n : ℕ) (R : Type _) [Ring R] : cyclotomic n R ∣ X ^ n - 1 := +theorem cyclotomic.dvd_X_pow_sub_one (n : ℕ) (R : Type _) [Ring R] : cyclotomic n R ∣ X ^ n - 1 := by suffices cyclotomic n ℤ ∣ X ^ n - 1 by simpa only [map_cyclotomic_int, Polynomial.map_sub, Polynomial.map_one, Polynomial.map_pow, @@ -404,7 +440,7 @@ theorem cyclotomic.dvd_x_pow_sub_one (n : ℕ) (R : Type _) [Ring R] : cyclotomi · simp rw [← prod_cyclotomic_eq_X_pow_sub_one hn] exact Finset.dvd_prod_of_mem _ (n.mem_divisors_self hn.ne') -#align polynomial.cyclotomic.dvd_X_pow_sub_one Polynomial.cyclotomic.dvd_x_pow_sub_one +#align polynomial.cyclotomic.dvd_X_pow_sub_one Polynomial.cyclotomic.dvd_X_pow_sub_one theorem prod_cyclotomic_eq_geom_sum {n : ℕ} (h : 0 < n) (R) [CommRing R] : (∏ i in n.divisors.eraseₓ 1, cyclotomic i R) = ∑ i in Finset.range n, X ^ i := @@ -427,13 +463,15 @@ theorem cyclotomic_prime (R : Type _) [Ring R] (p : ℕ) [hp : Fact p.Prime] : erase_insert (mem_singleton.not.2 hp.out.ne_one.symm), prod_singleton] #align polynomial.cyclotomic_prime Polynomial.cyclotomic_prime -theorem cyclotomic_prime_mul_x_sub_one (R : Type _) [Ring R] (p : ℕ) [hn : Fact (Nat.Prime p)] : +theorem cyclotomic_prime_mul_X_sub_one (R : Type _) [Ring R] (p : ℕ) [hn : Fact (Nat.Prime p)] : cyclotomic p R * (X - 1) = X ^ p - 1 := by rw [cyclotomic_prime, geom_sum_mul] -#align polynomial.cyclotomic_prime_mul_X_sub_one Polynomial.cyclotomic_prime_mul_x_sub_one +#align polynomial.cyclotomic_prime_mul_X_sub_one Polynomial.cyclotomic_prime_mul_X_sub_one +#print Polynomial.cyclotomic_two /- @[simp] theorem cyclotomic_two (R : Type _) [Ring R] : cyclotomic 2 R = X + 1 := by simp [cyclotomic_prime] #align polynomial.cyclotomic_two Polynomial.cyclotomic_two +-/ @[simp] theorem cyclotomic_three (R : Type _) [Ring R] : cyclotomic 3 R = X ^ 2 + X + 1 := by @@ -453,7 +491,7 @@ theorem cyclotomic_dvd_geom_sum_of_dvd (R) [Ring R] {d n : ℕ} (hdn : d ∣ n) simp [hd, hdn, hn.ne'] #align polynomial.cyclotomic_dvd_geom_sum_of_dvd Polynomial.cyclotomic_dvd_geom_sum_of_dvd -theorem x_pow_sub_one_mul_prod_cyclotomic_eq_x_pow_sub_one_of_dvd (R) [CommRing R] {d n : ℕ} +theorem X_pow_sub_one_mul_prod_cyclotomic_eq_X_pow_sub_one_of_dvd (R) [CommRing R] {d n : ℕ} (h : d ∈ n.properDivisors) : ((X ^ d - 1) * ∏ x in n.divisors \ d.divisors, cyclotomic x R) = X ^ n - 1 := by @@ -462,9 +500,9 @@ theorem x_pow_sub_one_mul_prod_cyclotomic_eq_x_pow_sub_one_of_dvd (R) [CommRing have h0d : 0 < d := Nat.pos_of_dvd_of_pos hd h0n rw [← prod_cyclotomic_eq_X_pow_sub_one h0d, ← prod_cyclotomic_eq_X_pow_sub_one h0n, mul_comm, Finset.prod_sdiff (Nat.divisors_subset_of_dvd h0n.ne' hd)] -#align polynomial.X_pow_sub_one_mul_prod_cyclotomic_eq_X_pow_sub_one_of_dvd Polynomial.x_pow_sub_one_mul_prod_cyclotomic_eq_x_pow_sub_one_of_dvd +#align polynomial.X_pow_sub_one_mul_prod_cyclotomic_eq_X_pow_sub_one_of_dvd Polynomial.X_pow_sub_one_mul_prod_cyclotomic_eq_X_pow_sub_one_of_dvd -theorem x_pow_sub_one_mul_cyclotomic_dvd_x_pow_sub_one_of_dvd (R) [CommRing R] {d n : ℕ} +theorem X_pow_sub_one_mul_cyclotomic_dvd_X_pow_sub_one_of_dvd (R) [CommRing R] {d n : ℕ} (h : d ∈ n.properDivisors) : (X ^ d - 1) * cyclotomic n R ∣ X ^ n - 1 := by have hdn := (nat.mem_proper_divisors.mp h).2 @@ -476,7 +514,7 @@ theorem x_pow_sub_one_mul_cyclotomic_dvd_x_pow_sub_one_of_dvd (R) [CommRing R] { rw [← Nat.insert_self_properDivisors hdn.ne_bot, insert_sdiff_of_not_mem, prod_insert] · exact Finset.not_mem_sdiff_of_not_mem_left Nat.properDivisors.not_self_mem · exact fun hk => hdn.not_le <| Nat.divisor_le hk -#align polynomial.X_pow_sub_one_mul_cyclotomic_dvd_X_pow_sub_one_of_dvd Polynomial.x_pow_sub_one_mul_cyclotomic_dvd_x_pow_sub_one_of_dvd +#align polynomial.X_pow_sub_one_mul_cyclotomic_dvd_X_pow_sub_one_of_dvd Polynomial.X_pow_sub_one_mul_cyclotomic_dvd_X_pow_sub_one_of_dvd section ArithmeticFunction @@ -486,7 +524,7 @@ open scoped ArithmeticFunction /-- `cyclotomic n R` can be expressed as a product in a fraction field of `R[X]` using Möbius inversion. -/ -theorem cyclotomic_eq_prod_x_pow_sub_one_pow_moebius {n : ℕ} (R : Type _) [CommRing R] +theorem cyclotomic_eq_prod_X_pow_sub_one_pow_moebius {n : ℕ} (R : Type _) [CommRing R] [IsDomain R] : algebraMap _ (RatFunc R) (cyclotomic n R) = ∏ i in n.divisorsAntidiagonal, algebraMap R[X] _ (X ^ i.snd - 1) ^ μ i.fst := @@ -506,13 +544,13 @@ theorem cyclotomic_eq_prod_x_pow_sub_one_pow_moebius {n : ℕ} (R : Type _) [Com · apply cyclotomic_ne_zero · apply monic.ne_zero apply monic_X_pow_sub_C _ (ne_of_gt hn) -#align polynomial.cyclotomic_eq_prod_X_pow_sub_one_pow_moebius Polynomial.cyclotomic_eq_prod_x_pow_sub_one_pow_moebius +#align polynomial.cyclotomic_eq_prod_X_pow_sub_one_pow_moebius Polynomial.cyclotomic_eq_prod_X_pow_sub_one_pow_moebius end ArithmeticFunction /-- We have `cyclotomic n R = (X ^ k - 1) /ₘ (∏ i in nat.proper_divisors k, cyclotomic i K)`. -/ -theorem cyclotomic_eq_x_pow_sub_one_div {R : Type _} [CommRing R] {n : ℕ} (hpos : 0 < n) : +theorem cyclotomic_eq_X_pow_sub_one_div {R : Type _} [CommRing R] {n : ℕ} (hpos : 0 < n) : cyclotomic n R = (X ^ n - 1) /ₘ ∏ i in Nat.properDivisors n, cyclotomic i R := by nontriviality R @@ -530,11 +568,11 @@ theorem cyclotomic_eq_x_pow_sub_one_div {R : Type _} [CommRing R] {n : ℕ} (hpo rw [bot_lt_iff_ne_bot] intro h exact monic.ne_zero prod_monic (degree_eq_bot.1 h) -#align polynomial.cyclotomic_eq_X_pow_sub_one_div Polynomial.cyclotomic_eq_x_pow_sub_one_div +#align polynomial.cyclotomic_eq_X_pow_sub_one_div Polynomial.cyclotomic_eq_X_pow_sub_one_div /-- If `m` is a proper divisor of `n`, then `X ^ m - 1` divides `∏ i in nat.proper_divisors n, cyclotomic i R`. -/ -theorem x_pow_sub_one_dvd_prod_cyclotomic (R : Type _) [CommRing R] {n m : ℕ} (hpos : 0 < n) +theorem X_pow_sub_one_dvd_prod_cyclotomic (R : Type _) [CommRing R] {n m : ℕ} (hpos : 0 < n) (hm : m ∣ n) (hdiff : m ≠ n) : X ^ m - 1 ∣ ∏ i in Nat.properDivisors n, cyclotomic i R := by replace hm := @@ -547,12 +585,12 @@ theorem x_pow_sub_one_dvd_prod_cyclotomic (R : Type _) [CommRing R] {n m : ℕ} Finset.prod_union Finset.sdiff_disjoint, prod_cyclotomic_eq_X_pow_sub_one (Nat.pos_of_mem_properDivisors hm)] exact ⟨∏ x : ℕ in n.proper_divisors \ m.divisors, cyclotomic x R, by rw [mul_comm]⟩ -#align polynomial.X_pow_sub_one_dvd_prod_cyclotomic Polynomial.x_pow_sub_one_dvd_prod_cyclotomic +#align polynomial.X_pow_sub_one_dvd_prod_cyclotomic Polynomial.X_pow_sub_one_dvd_prod_cyclotomic /-- If there is a primitive `n`-th root of unity in `K`, then `cyclotomic n K = ∏ μ in primitive_roots n R, (X - C μ)`. In particular, `cyclotomic n K = cyclotomic' n K` -/ -theorem cyclotomic_eq_prod_x_sub_primitiveRoots {K : Type _} [CommRing K] [IsDomain K] {ζ : K} +theorem cyclotomic_eq_prod_X_sub_primitiveRoots {K : Type _} [CommRing K] [IsDomain K] {ζ : K} {n : ℕ} (hz : IsPrimitiveRoot ζ n) : cyclotomic n K = ∏ μ in primitiveRoots n K, X - C μ := by rw [← cyclotomic'] @@ -567,7 +605,7 @@ theorem cyclotomic_eq_prod_x_sub_primitiveRoots {K : Type _} [CommRing K] [IsDom exact hk i (Nat.mem_properDivisors.1 hi).2 (IsPrimitiveRoot.pow hpos hz hd) rw [@cyclotomic_eq_X_pow_sub_one_div _ _ _ hpos, cyclotomic'_eq_X_pow_sub_one_div hpos hz, Finset.prod_congr (refl k.proper_divisors) h] -#align polynomial.cyclotomic_eq_prod_X_sub_primitive_roots Polynomial.cyclotomic_eq_prod_x_sub_primitiveRoots +#align polynomial.cyclotomic_eq_prod_X_sub_primitive_roots Polynomial.cyclotomic_eq_prod_X_sub_primitiveRoots theorem eq_cyclotomic_iff {R : Type _} [CommRing R] {n : ℕ} (hpos : 0 < n) (P : R[X]) : P = cyclotomic n R ↔ (P * ∏ i in Nat.properDivisors n, Polynomial.cyclotomic i R) = X ^ n - 1 := @@ -613,11 +651,11 @@ theorem cyclotomic_prime_pow_eq_geom_sum {R : Type _} [CommRing R] {p n : ℕ} ( rw [mul_comm _ (∑ i in _, _), n_ih, geom_sum_mul, sub_left_inj, ← pow_mul, pow_add, pow_one] #align polynomial.cyclotomic_prime_pow_eq_geom_sum Polynomial.cyclotomic_prime_pow_eq_geom_sum -theorem cyclotomic_prime_pow_mul_x_pow_sub_one (R : Type _) [CommRing R] (p k : ℕ) +theorem cyclotomic_prime_pow_mul_X_pow_sub_one (R : Type _) [CommRing R] (p k : ℕ) [hn : Fact (Nat.Prime p)] : cyclotomic (p ^ (k + 1)) R * (X ^ p ^ k - 1) = X ^ p ^ (k + 1) - 1 := by rw [cyclotomic_prime_pow_eq_geom_sum hn.out, geom_sum_mul, ← pow_mul, pow_succ, mul_comm] -#align polynomial.cyclotomic_prime_pow_mul_X_pow_sub_one Polynomial.cyclotomic_prime_pow_mul_x_pow_sub_one +#align polynomial.cyclotomic_prime_pow_mul_X_pow_sub_one Polynomial.cyclotomic_prime_pow_mul_X_pow_sub_one /-- The constant term of `cyclotomic n R` is `1` if `2 ≤ n`. -/ theorem cyclotomic_coeff_zero (R : Type _) [CommRing R] {n : ℕ} (hn : 1 < n) : diff --git a/Mathbin/RingTheory/RootsOfUnity/Basic.lean b/Mathbin/RingTheory/RootsOfUnity/Basic.lean index a9224b399d..bed7528586 100644 --- a/Mathbin/RingTheory/RootsOfUnity/Basic.lean +++ b/Mathbin/RingTheory/RootsOfUnity/Basic.lean @@ -97,9 +97,9 @@ theorem mem_rootsOfUnity (k : ℕ+) (ζ : Mˣ) : ζ ∈ rootsOfUnity k M ↔ ζ Iff.rfl #align mem_roots_of_unity mem_rootsOfUnity -theorem mem_roots_of_unity' (k : ℕ+) (ζ : Mˣ) : ζ ∈ rootsOfUnity k M ↔ (ζ : M) ^ (k : ℕ) = 1 := by +theorem mem_rootsOfUnity' (k : ℕ+) (ζ : Mˣ) : ζ ∈ rootsOfUnity k M ↔ (ζ : M) ^ (k : ℕ) = 1 := by rw [mem_rootsOfUnity]; norm_cast -#align mem_roots_of_unity' mem_roots_of_unity' +#align mem_roots_of_unity' mem_rootsOfUnity' theorem rootsOfUnity.coe_injective {n : ℕ+} : Function.Injective (coe : rootsOfUnity n M → M) := Units.ext.comp fun x y => Subtype.ext @@ -259,7 +259,7 @@ theorem card_rootsOfUnity : Fintype.card (rootsOfUnity k R) ≤ k := variable {k R} -theorem map_root_of_unity_eq_pow_self [RingHomClass F R R] (σ : F) (ζ : rootsOfUnity k R) : +theorem map_rootsOfUnity_eq_pow_self [RingHomClass F R R] (σ : F) (ζ : rootsOfUnity k R) : ∃ m : ℕ, σ ζ = ζ ^ m := by obtain ⟨m, hm⟩ := MonoidHom.map_cyclic (restrictRootsOfUnity σ k) @@ -268,7 +268,7 @@ theorem map_root_of_unity_eq_pow_self [RingHomClass F R R] (σ : F) (ζ : rootsO (m.mod_nonneg (int.coe_nat_ne_zero.mpr (pos_iff_ne_zero.mp (orderOf_pos ζ)))), zpow_ofNat, rootsOfUnity.coe_pow] exact ⟨(m % orderOf ζ).toNat, rfl⟩ -#align map_root_of_unity_eq_pow_self map_root_of_unity_eq_pow_self +#align map_root_of_unity_eq_pow_self map_rootsOfUnity_eq_pow_self end IsDomain @@ -279,19 +279,21 @@ variable (R) [CommRing R] [IsReduced R] @[simp] theorem mem_rootsOfUnity_prime_pow_mul_iff (p k : ℕ) (m : ℕ+) [hp : Fact p.Prime] [CharP R p] {ζ : Rˣ} : ζ ∈ rootsOfUnity (⟨p, hp.1.Pos⟩ ^ k * m) R ↔ ζ ∈ rootsOfUnity m R := by - simp [mem_roots_of_unity'] + simp [mem_rootsOfUnity'] #align mem_roots_of_unity_prime_pow_mul_iff mem_rootsOfUnity_prime_pow_mul_iff end Reduced end rootsOfUnity +#print IsPrimitiveRoot /- /-- An element `ζ` is a primitive `k`-th root of unity if `ζ ^ k = 1`, and if `l` satisfies `ζ ^ l = 1` then `k ∣ l`. -/ structure IsPrimitiveRoot (ζ : M) (k : ℕ) : Prop where pow_eq_one : ζ ^ (k : ℕ) = 1 dvd_of_pow_eq_one : ∀ l : ℕ, ζ ^ l = 1 → k ∣ l #align is_primitive_root IsPrimitiveRoot +-/ /-- Turn a primitive root μ into a member of the `roots_of_unity` subgroup. -/ @[simps] @@ -303,31 +305,39 @@ section primitiveRoots variable {k : ℕ} +#print primitiveRoots /- /-- `primitive_roots k R` is the finset of primitive `k`-th roots of unity in the integral domain `R`. -/ def primitiveRoots (k : ℕ) (R : Type _) [CommRing R] [IsDomain R] : Finset R := (nthRoots k (1 : R)).toFinset.filterₓ fun ζ => IsPrimitiveRoot ζ k #align primitive_roots primitiveRoots +-/ variable [CommRing R] [IsDomain R] +#print mem_primitiveRoots /- @[simp] theorem mem_primitiveRoots {ζ : R} (h0 : 0 < k) : ζ ∈ primitiveRoots k R ↔ IsPrimitiveRoot ζ k := by rw [primitiveRoots, mem_filter, Multiset.mem_toFinset, mem_nth_roots h0, and_iff_right_iff_imp] exact IsPrimitiveRoot.pow_eq_one #align mem_primitive_roots mem_primitiveRoots +-/ +#print primitiveRoots_zero /- @[simp] theorem primitiveRoots_zero : primitiveRoots 0 R = ∅ := by rw [primitiveRoots, nth_roots_zero, Multiset.toFinset_zero, Finset.filter_empty] #align primitive_roots_zero primitiveRoots_zero +-/ +#print isPrimitiveRoot_of_mem_primitiveRoots /- theorem isPrimitiveRoot_of_mem_primitiveRoots {ζ : R} (h : ζ ∈ primitiveRoots k R) : IsPrimitiveRoot ζ k := k.eq_zero_or_pos.elim (fun hk => False.elim <| by simpa [hk] using h) fun hk => (mem_primitiveRoots hk).1 h #align is_primitive_root_of_mem_primitive_roots isPrimitiveRoot_of_mem_primitiveRoots +-/ end primitiveRoots @@ -353,21 +363,25 @@ section CommMonoid variable {ζ : M} {f : F} (h : IsPrimitiveRoot ζ k) +#print IsPrimitiveRoot.of_subsingleton /- @[nontriviality] theorem of_subsingleton [Subsingleton M] (x : M) : IsPrimitiveRoot x 1 := ⟨Subsingleton.elim _ _, fun _ _ => one_dvd _⟩ #align is_primitive_root.of_subsingleton IsPrimitiveRoot.of_subsingleton +-/ theorem pow_eq_one_iff_dvd (l : ℕ) : ζ ^ l = 1 ↔ k ∣ l := ⟨h.dvd_of_pow_eq_one l, by rintro ⟨i, rfl⟩; simp only [pow_mul, h.pow_eq_one, one_pow, PNat.mul_coe]⟩ #align is_primitive_root.pow_eq_one_iff_dvd IsPrimitiveRoot.pow_eq_one_iff_dvd +#print IsPrimitiveRoot.isUnit /- theorem isUnit (h : IsPrimitiveRoot ζ k) (h0 : 0 < k) : IsUnit ζ := by apply isUnit_of_mul_eq_one ζ (ζ ^ (k - 1)) rw [← pow_succ, tsub_add_cancel_of_le h0.nat_succ_le, h.pow_eq_one] #align is_primitive_root.is_unit IsPrimitiveRoot.isUnit +-/ theorem pow_ne_one_of_pos_of_lt (h0 : 0 < l) (hl : l < k) : ζ ^ l ≠ 1 := mt (Nat.le_of_dvd h0 ∘ h.dvd_of_pow_eq_one _) <| not_le_of_lt hl @@ -377,6 +391,7 @@ theorem ne_one (hk : 1 < k) : ζ ≠ 1 := h.pow_ne_one_of_pos_of_lt zero_lt_one hk ∘ (pow_one ζ).trans #align is_primitive_root.ne_one IsPrimitiveRoot.ne_one +#print IsPrimitiveRoot.pow_inj /- theorem pow_inj (h : IsPrimitiveRoot ζ k) ⦃i j : ℕ⦄ (hi : i < k) (hj : j < k) (H : ζ ^ i = ζ ^ j) : i = j := by wlog hij : i ≤ j generalizing i j @@ -388,6 +403,7 @@ theorem pow_inj (h : IsPrimitiveRoot ζ k) ⦃i j : ℕ⦄ (hi : i < k) (hj : j rw [← ((h.is_unit (lt_of_le_of_lt (Nat.zero_le _) hi)).pow i).mul_left_inj, ← pow_add, tsub_add_cancel_of_le hij, H, one_mul] #align is_primitive_root.pow_inj IsPrimitiveRoot.pow_inj +-/ theorem one : IsPrimitiveRoot (1 : M) 1 := { pow_eq_one := pow_one _ @@ -408,11 +424,14 @@ theorem coe_submonoidClass_iff {M B : Type _} [CommMonoid M] [SetLike B M] [Subm simp [iff_def, ← SubmonoidClass.coe_pow] #align is_primitive_root.coe_submonoid_class_iff IsPrimitiveRoot.coe_submonoidClass_iff +#print IsPrimitiveRoot.coe_units_iff /- @[simp] theorem coe_units_iff {ζ : Mˣ} : IsPrimitiveRoot (ζ : M) k ↔ IsPrimitiveRoot ζ k := by simp only [iff_def, Units.ext_iff, Units.val_pow_eq_pow_val, Units.val_one] #align is_primitive_root.coe_units_iff IsPrimitiveRoot.coe_units_iff +-/ +#print IsPrimitiveRoot.pow_of_coprime /- theorem pow_of_coprime (h : IsPrimitiveRoot ζ k) (i : ℕ) (hi : i.coprime k) : IsPrimitiveRoot (ζ ^ i) k := by by_cases h0 : k = 0 @@ -429,13 +448,17 @@ theorem pow_of_coprime (h : IsPrimitiveRoot ζ k) (i : ℕ) (hi : i.coprime k) : zpow_ofNat, ← zpow_mul, mul_right_comm] simp only [zpow_mul, hl, h.pow_eq_one, one_zpow, one_pow, one_mul, zpow_ofNat] #align is_primitive_root.pow_of_coprime IsPrimitiveRoot.pow_of_coprime +-/ +#print IsPrimitiveRoot.pow_of_prime /- theorem pow_of_prime (h : IsPrimitiveRoot ζ k) {p : ℕ} (hprime : Nat.Prime p) (hdiv : ¬p ∣ k) : IsPrimitiveRoot (ζ ^ p) k := h.pow_of_coprime p (hprime.coprime_iff_not_dvd.2 hdiv) #align is_primitive_root.pow_of_prime IsPrimitiveRoot.pow_of_prime +-/ /- ./././Mathport/Syntax/Translate/Tactic/Lean3.lean:132:4: warning: unsupported: rw with cfg: { occs := occurrences.pos[occurrences.pos] «expr[ ,]»([1]) } -/ +#print IsPrimitiveRoot.pow_iff_coprime /- theorem pow_iff_coprime (h : IsPrimitiveRoot ζ k) (h0 : 0 < k) (i : ℕ) : IsPrimitiveRoot (ζ ^ i) k ↔ i.coprime k := by @@ -449,18 +472,25 @@ theorem pow_iff_coprime (h : IsPrimitiveRoot ζ k) (h0 : 0 < k) (i : ℕ) : apply Nat.dvd_antisymm ⟨i.gcd k, hb⟩ (hi.dvd_of_pow_eq_one b _) rw [← pow_mul', ← mul_assoc, ← hb, pow_mul, h.pow_eq_one, one_pow] #align is_primitive_root.pow_iff_coprime IsPrimitiveRoot.pow_iff_coprime +-/ +#print IsPrimitiveRoot.orderOf /- protected theorem orderOf (ζ : M) : IsPrimitiveRoot ζ (orderOf ζ) := ⟨pow_orderOf_eq_one ζ, fun l => orderOf_dvd_of_pow_eq_one⟩ #align is_primitive_root.order_of IsPrimitiveRoot.orderOf +-/ +#print IsPrimitiveRoot.unique /- theorem unique {ζ : M} (hk : IsPrimitiveRoot ζ k) (hl : IsPrimitiveRoot ζ l) : k = l := Nat.dvd_antisymm (hk.2 _ hl.1) (hl.2 _ hk.1) #align is_primitive_root.unique IsPrimitiveRoot.unique +-/ +#print IsPrimitiveRoot.eq_orderOf /- theorem eq_orderOf : k = orderOf ζ := h.unique (IsPrimitiveRoot.orderOf ζ) #align is_primitive_root.eq_order_of IsPrimitiveRoot.eq_orderOf +-/ protected theorem iff (hk : 0 < k) : IsPrimitiveRoot ζ k ↔ ζ ^ k = 1 ∧ ∀ l : ℕ, 0 < l → l < k → ζ ^ l ≠ 1 := @@ -472,23 +502,28 @@ protected theorem iff (hk : 0 < k) : exact pow_ne_one_of_lt_orderOf' hl'.ne' hl #align is_primitive_root.iff IsPrimitiveRoot.iff +#print IsPrimitiveRoot.not_iff /- protected theorem not_iff : ¬IsPrimitiveRoot ζ k ↔ orderOf ζ ≠ k := ⟨fun h hk => h <| hk ▸ IsPrimitiveRoot.orderOf ζ, fun h hk => h.symm <| hk.unique <| IsPrimitiveRoot.orderOf ζ⟩ #align is_primitive_root.not_iff IsPrimitiveRoot.not_iff +-/ +#print IsPrimitiveRoot.pow_of_dvd /- theorem pow_of_dvd (h : IsPrimitiveRoot ζ k) {p : ℕ} (hp : p ≠ 0) (hdiv : p ∣ k) : IsPrimitiveRoot (ζ ^ p) (k / p) := by suffices orderOf (ζ ^ p) = k / p by exact this ▸ IsPrimitiveRoot.orderOf (ζ ^ p) rw [orderOf_pow' _ hp, ← eq_order_of h, Nat.gcd_eq_right hdiv] #align is_primitive_root.pow_of_dvd IsPrimitiveRoot.pow_of_dvd +-/ protected theorem mem_rootsOfUnity {ζ : Mˣ} {n : ℕ+} (h : IsPrimitiveRoot ζ n) : ζ ∈ rootsOfUnity n M := h.pow_eq_one #align is_primitive_root.mem_roots_of_unity IsPrimitiveRoot.mem_rootsOfUnity +#print IsPrimitiveRoot.pow /- /-- If there is a `n`-th primitive root of unity in `R` and `b` divides `n`, then there is a `b`-th primitive root of unity in `R`. -/ theorem pow {n : ℕ} {a b : ℕ} (hn : 0 < n) (h : IsPrimitiveRoot ζ n) (hprod : n = a * b) : @@ -500,6 +535,7 @@ theorem pow {n : ℕ} {a b : ℕ} (hn : 0 < n) (h : IsPrimitiveRoot ζ n) (hprod rwa [← mul_dvd_mul_iff_left ha0] exact h.dvd_of_pow_eq_one _ hl #align is_primitive_root.pow IsPrimitiveRoot.pow +-/ section Maps @@ -582,6 +618,7 @@ theorem inv_iff : IsPrimitiveRoot ζ⁻¹ k ↔ IsPrimitiveRoot ζ k := by refin intro h; rw [← inv_inv ζ]; exact inv h #align is_primitive_root.inv_iff IsPrimitiveRoot.inv_iff +#print IsPrimitiveRoot.zpow_of_gcd_eq_one /- theorem zpow_of_gcd_eq_one (h : IsPrimitiveRoot ζ k) (i : ℤ) (hi : i.gcd k = 1) : IsPrimitiveRoot (ζ ^ i) k := by by_cases h0 : 0 ≤ i @@ -595,6 +632,7 @@ theorem zpow_of_gcd_eq_one (h : IsPrimitiveRoot ζ k) (i : ℤ) (hi : i.gcd k = rw [Int.gcd, ← Int.natAbs_neg, ← hi'] at hi exact hi #align is_primitive_root.zpow_of_gcd_eq_one IsPrimitiveRoot.zpow_of_gcd_eq_one +-/ end DivisionCommMonoid @@ -639,9 +677,11 @@ theorem ne_zero' {n : ℕ+} (hζ : IsPrimitiveRoot ζ n) : NeZero ((n : ℕ) : R · exact NeZero.of_not_dvd R hp #align is_primitive_root.ne_zero' IsPrimitiveRoot.ne_zero' +#print IsPrimitiveRoot.mem_nthRootsFinset /- theorem mem_nthRootsFinset (hζ : IsPrimitiveRoot ζ k) (hk : 0 < k) : ζ ∈ nthRootsFinset k R := (mem_nthRootsFinset hk).2 hζ.pow_eq_one #align is_primitive_root.mem_nth_roots_finset IsPrimitiveRoot.mem_nthRootsFinset +-/ end IsDomain @@ -811,7 +851,7 @@ theorem isPrimitiveRoot_iff {k : ℕ} {ζ ξ : R} (h : IsPrimitiveRoot ζ k) (h0 · rintro ⟨i, -, hi, rfl⟩; exact h.pow_of_coprime i hi #align is_primitive_root.is_primitive_root_iff IsPrimitiveRoot.isPrimitiveRoot_iff -theorem card_roots_of_unity' {n : ℕ+} (h : IsPrimitiveRoot ζ n) : +theorem card_rootsOfUnity' {n : ℕ+} (h : IsPrimitiveRoot ζ n) : Fintype.card (rootsOfUnity n R) = n := by let e := h.zmod_equiv_zpowers @@ -822,7 +862,7 @@ theorem card_roots_of_unity' {n : ℕ+} (h : IsPrimitiveRoot ζ n) : _ = Fintype.card (ZMod n) := (Fintype.card_congr e.to_equiv.symm) _ = n := ZMod.card n -#align is_primitive_root.card_roots_of_unity' IsPrimitiveRoot.card_roots_of_unity' +#align is_primitive_root.card_roots_of_unity' IsPrimitiveRoot.card_rootsOfUnity' theorem card_rootsOfUnity {ζ : R} {n : ℕ+} (h : IsPrimitiveRoot ζ n) : Fintype.card (rootsOfUnity n R) = n := @@ -876,14 +916,17 @@ theorem nthRoots_nodup {ζ : R} {n : ℕ} (h : IsPrimitiveRoot ζ n) : (nthRoots exact Nat.lt_asymm ha ha #align is_primitive_root.nth_roots_nodup IsPrimitiveRoot.nthRoots_nodup +#print IsPrimitiveRoot.card_nthRootsFinset /- @[simp] theorem card_nthRootsFinset {ζ : R} {n : ℕ} (h : IsPrimitiveRoot ζ n) : (nthRootsFinset n R).card = n := by rw [nth_roots_finset, ← Multiset.toFinset_eq (nth_roots_nodup h), card_mk, h.card_nth_roots] #align is_primitive_root.card_nth_roots_finset IsPrimitiveRoot.card_nthRootsFinset +-/ open scoped Nat +#print IsPrimitiveRoot.card_primitiveRoots /- /-- If an integral domain has a primitive `k`-th root of unity, then it has `φ k` of them. -/ theorem card_primitiveRoots {ζ : R} {k : ℕ} (h : IsPrimitiveRoot ζ k) : (primitiveRoots k R).card = φ k := by @@ -905,6 +948,7 @@ theorem card_primitiveRoots {ζ : R} {k : ℕ} (h : IsPrimitiveRoot ζ k) : rcases hξ with ⟨i, hin, hi, H⟩ exact ⟨i, ⟨hin, hi.symm⟩, H⟩ #align is_primitive_root.card_primitive_roots IsPrimitiveRoot.card_primitiveRoots +-/ /-- The sets `primitive_roots k R` are pairwise disjoint. -/ theorem disjoint {k l : ℕ} (h : k ≠ l) : Disjoint (primitiveRoots k R) (primitiveRoots l R) := @@ -913,10 +957,11 @@ theorem disjoint {k l : ℕ} (h : k ≠ l) : Disjoint (primitiveRoots k R) (prim (isPrimitiveRoot_of_mem_primitiveRoots hk).unique <| isPrimitiveRoot_of_mem_primitiveRoots hl #align is_primitive_root.disjoint IsPrimitiveRoot.disjoint +#print IsPrimitiveRoot.nthRoots_one_eq_biUnion_primitiveRoots' /- /-- `nth_roots n` as a `finset` is equal to the union of `primitive_roots i R` for `i ∣ n` if there is a primitive root of unity in `R`. This holds for any `nat`, not just `pnat`, see `nth_roots_one_eq_bUnion_primitive_roots`. -/ -theorem nth_roots_one_eq_biUnion_primitive_roots' {ζ : R} {n : ℕ+} (h : IsPrimitiveRoot ζ n) : +theorem nthRoots_one_eq_biUnion_primitiveRoots' {ζ : R} {n : ℕ+} (h : IsPrimitiveRoot ζ n) : nthRootsFinset n R = (Nat.divisors ↑n).biUnion fun i => primitiveRoots i R := by symm @@ -942,17 +987,20 @@ theorem nth_roots_one_eq_biUnion_primitive_roots' {ζ : R} {n : ℕ+} (h : IsPri rw [(h.pow n.pos hd).card_primitiveRoots] · intro i hi j hj hdiff exact Disjoint hdiff -#align is_primitive_root.nth_roots_one_eq_bUnion_primitive_roots' IsPrimitiveRoot.nth_roots_one_eq_biUnion_primitive_roots' +#align is_primitive_root.nth_roots_one_eq_bUnion_primitive_roots' IsPrimitiveRoot.nthRoots_one_eq_biUnion_primitiveRoots' +-/ +#print IsPrimitiveRoot.nthRoots_one_eq_biUnion_primitiveRoots /- /-- `nth_roots n` as a `finset` is equal to the union of `primitive_roots i R` for `i ∣ n` if there is a primitive root of unity in `R`. -/ -theorem nth_roots_one_eq_biUnion_primitiveRoots {ζ : R} {n : ℕ} (h : IsPrimitiveRoot ζ n) : +theorem nthRoots_one_eq_biUnion_primitiveRoots {ζ : R} {n : ℕ} (h : IsPrimitiveRoot ζ n) : nthRootsFinset n R = (Nat.divisors n).biUnion fun i => primitiveRoots i R := by by_cases hn : n = 0 · simp [hn] exact @nth_roots_one_eq_bUnion_primitive_roots' _ _ _ _ ⟨n, Nat.pos_of_ne_zero hn⟩ h -#align is_primitive_root.nth_roots_one_eq_bUnion_primitive_roots IsPrimitiveRoot.nth_roots_one_eq_biUnion_primitiveRoots +#align is_primitive_root.nth_roots_one_eq_bUnion_primitive_roots IsPrimitiveRoot.nthRoots_one_eq_biUnion_primitiveRoots +-/ end IsDomain @@ -968,7 +1016,7 @@ noncomputable def autToPow : (S ≃ₐ[R] S) →* (ZMod n)ˣ := have ho : orderOf μ' = n := by rw [hμ.eq_order_of, ← hμ.coe_to_roots_of_unity_coe, orderOf_units, orderOf_subgroup] MonoidHom.toHomUnits - { toFun := fun σ => (map_root_of_unity_eq_pow_self σ.toAlgHom μ').some + { toFun := fun σ => (map_rootsOfUnity_eq_pow_self σ.toAlgHom μ').some map_one' := by generalize_proofs h1 have h := h1.some_spec @@ -998,7 +1046,7 @@ noncomputable def autToPow : (S ≃ₐ[R] S) →* (ZMod n)ˣ := -- We are not using @[simps] in aut_to_pow to avoid a timeout. theorem coe_autToPow_apply (f : S ≃ₐ[R] S) : (autToPow R hμ f : ZMod n) = - ((map_root_of_unity_eq_pow_self f hμ.toRootsOfUnity).some : ZMod n) := + ((map_rootsOfUnity_eq_pow_self f hμ.toRootsOfUnity).some : ZMod n) := rfl #align is_primitive_root.coe_aut_to_pow_apply IsPrimitiveRoot.coe_autToPow_apply diff --git a/Mathbin/RingTheory/RootsOfUnity/Complex.lean b/Mathbin/RingTheory/RootsOfUnity/Complex.lean index 63b4fa2359..2f5390e598 100644 --- a/Mathbin/RingTheory/RootsOfUnity/Complex.lean +++ b/Mathbin/RingTheory/RootsOfUnity/Complex.lean @@ -94,12 +94,14 @@ theorem card_rootsOfUnity (n : ℕ+) : Fintype.card (rootsOfUnity n ℂ) = n := (isPrimitiveRoot_exp n n.NeZero).card_rootsOfUnity #align complex.card_roots_of_unity Complex.card_rootsOfUnity +#print Complex.card_primitiveRoots /- theorem card_primitiveRoots (k : ℕ) : (primitiveRoots k ℂ).card = φ k := by by_cases h : k = 0 · simp [h] exact (is_primitive_root_exp k h).card_primitiveRoots #align complex.card_primitive_roots Complex.card_primitiveRoots +-/ end Complex @@ -113,10 +115,12 @@ theorem IsPrimitiveRoot.nnnorm_eq_one {ζ : ℂ} {n : ℕ} (h : IsPrimitiveRoot Subtype.ext <| h.norm'_eq_one hn #align is_primitive_root.nnnorm_eq_one IsPrimitiveRoot.nnnorm_eq_one +#print IsPrimitiveRoot.arg_ext /- theorem IsPrimitiveRoot.arg_ext {n m : ℕ} {ζ μ : ℂ} (hζ : IsPrimitiveRoot ζ n) (hμ : IsPrimitiveRoot μ m) (hn : n ≠ 0) (hm : m ≠ 0) (h : ζ.arg = μ.arg) : ζ = μ := Complex.ext_abs_arg ((hζ.norm'_eq_one hn).trans (hμ.norm'_eq_one hm).symm) h #align is_primitive_root.arg_ext IsPrimitiveRoot.arg_ext +-/ theorem IsPrimitiveRoot.arg_eq_zero_iff {n : ℕ} {ζ : ℂ} (hζ : IsPrimitiveRoot ζ n) (hn : n ≠ 0) : ζ.arg = 0 ↔ ζ = 1 := diff --git a/lake-manifest.json b/lake-manifest.json index e814edd34a..40e57aa3cf 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -2,17 +2,23 @@ "packagesDir": "lake-packages", "packages": [{"git": + {"url": "https://github.com/EdAyers/ProofWidgets4", + "subDir?": null, + "rev": "3b157dc3f6162615de001a8ebe7e01d629c97448", + "name": "proofwidgets", + "inputRev?": "v0.0.10"}}, + {"git": {"url": "https://github.com/leanprover-community/lean3port.git", "subDir?": null, - "rev": "e6a567ae2582a8617ffaa46c4d769dad17e96d31", + "rev": "ec058ed36485ea3917322645eb4c754a41810773", "name": "lean3port", - "inputRev?": "e6a567ae2582a8617ffaa46c4d769dad17e96d31"}}, + "inputRev?": "ec058ed36485ea3917322645eb4c754a41810773"}}, {"git": {"url": "https://github.com/leanprover-community/mathlib4.git", "subDir?": null, - "rev": "51cf59753a5b06fb822f05564a54f0a96746deab", + "rev": "f24c97ec2acd399fb2ce8c3f09f0d74aa9ebf300", "name": "mathlib", - "inputRev?": "51cf59753a5b06fb822f05564a54f0a96746deab"}}, + "inputRev?": "f24c97ec2acd399fb2ce8c3f09f0d74aa9ebf300"}}, {"git": {"url": "https://github.com/gebner/quote4", "subDir?": null, diff --git a/lakefile.lean b/lakefile.lean index bae8753272..deea3867d4 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -4,7 +4,7 @@ open Lake DSL System -- Usually the `tag` will be of the form `nightly-2021-11-22`. -- If you would like to use an artifact from a PR build, -- it will be of the form `pr-branchname-sha`. -def tag : String := "nightly-2023-06-07-11" +def tag : String := "nightly-2023-06-07-23" def releaseRepo : String := "leanprover-community/mathport" def oleanTarName : String := "mathlib3-binport.tar.gz" @@ -38,7 +38,7 @@ target fetchOleans (_pkg : Package) : Unit := do untarReleaseArtifact releaseRepo tag oleanTarName libDir return .nil -require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"e6a567ae2582a8617ffaa46c4d769dad17e96d31" +require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"ec058ed36485ea3917322645eb4c754a41810773" @[default_target] lean_lib Mathbin where