bump to nightly-2023-06-22-09

mathlib commit leanprover-community/mathlib@6285167

Mathbin/GroupTheory/Schreier.lean

@@ -146,15 +146,15 @@ theorem exists_finset_card_le_mul [FiniteIndex H] {S : Finset G} (hS : closure (
 #align subgroup.exists_finset_card_le_mul Subgroup.exists_finset_card_le_mul
 -/
 
-#print Subgroup.fG_of_index_ne_zero /-
+#print Subgroup.fg_of_index_ne_zero /-
 /-- **Schreier's Lemma**: A finite index subgroup of a finitely generated
   group is finitely generated. -/
-instance fG_of_index_ne_zero [hG : Group.FG G] [FiniteIndex H] : Group.FG H :=
+instance fg_of_index_ne_zero [hG : Group.FG G] [FiniteIndex H] : Group.FG H :=
   by
   obtain ⟨S, hS⟩ := hG.1
   obtain ⟨T, -, hT⟩ := exists_finset_card_le_mul H hS
   exact ⟨⟨T, hT⟩⟩
-#align subgroup.fg_of_index_ne_zero Subgroup.fG_of_index_ne_zero
+#align subgroup.fg_of_index_ne_zero Subgroup.fg_of_index_ne_zero
 -/
 
 #print Subgroup.rank_le_index_mul_rank /-

Mathbin/LinearAlgebra/CliffordAlgebra/Basic.lean

@@ -61,51 +61,62 @@ namespace CliffordAlgebra
 
 open TensorAlgebra
 
+#print CliffordAlgebra.Rel /-
 /-- `rel` relates each `ι m * ι m`, for `m : M`, with `Q m`.
 
 The Clifford algebra of `M` is defined as the quotient modulo this relation.
 -/
 inductive Rel : TensorAlgebra R M → TensorAlgebra R M → Prop
   | of (m : M) : Rel (ι R m * ι R m) (algebraMap R _ (Q m))
 #align clifford_algebra.rel CliffordAlgebra.Rel
+-/
 
 end CliffordAlgebra
 
 /- ./././Mathport/Syntax/Translate/Command.lean:43:9: unsupported derive handler algebra[algebra] R -/
+#print CliffordAlgebra /-
 /-- The Clifford algebra of an `R`-module `M` equipped with a quadratic_form `Q`.
 -/
 def CliffordAlgebra :=
   RingQuot (CliffordAlgebra.Rel Q)
 deriving Inhabited, Ring,
   «./././Mathport/Syntax/Translate/Command.lean:43:9: unsupported derive handler algebra[algebra] R»
 #align clifford_algebra CliffordAlgebra
+-/
 
 namespace CliffordAlgebra
 
+#print CliffordAlgebra.ι /-
 /-- The canonical linear map `M →ₗ[R] clifford_algebra Q`.
 -/
 def ι : M →ₗ[R] CliffordAlgebra Q :=
   (RingQuot.mkAlgHom R _).toLinearMap.comp (TensorAlgebra.ι R)
 #align clifford_algebra.ι CliffordAlgebra.ι
+-/
 
+#print CliffordAlgebra.ι_sq_scalar /-
 /-- As well as being linear, `ι Q` squares to the quadratic form -/
 @[simp]
 theorem ι_sq_scalar (m : M) : ι Q m * ι Q m = algebraMap R _ (Q m) :=
   by
   erw [← AlgHom.map_mul, RingQuot.mkAlgHom_rel R (rel.of m), AlgHom.commutes]
   rfl
 #align clifford_algebra.ι_sq_scalar CliffordAlgebra.ι_sq_scalar
+-/
 
 variable {Q} {A : Type _} [Semiring A] [Algebra R A]
 
+#print CliffordAlgebra.comp_ι_sq_scalar /-
 @[simp]
 theorem comp_ι_sq_scalar (g : CliffordAlgebra Q →ₐ[R] A) (m : M) :
     g (ι Q m) * g (ι Q m) = algebraMap _ _ (Q m) := by
   rw [← AlgHom.map_mul, ι_sq_scalar, AlgHom.commutes]
 #align clifford_algebra.comp_ι_sq_scalar CliffordAlgebra.comp_ι_sq_scalar
+-/
 
 variable (Q)
 
+#print CliffordAlgebra.lift /-
 /-- Given a linear map `f : M →ₗ[R] A` into an `R`-algebra `A`, which satisfies the condition:
 `cond : ∀ m : M, f m * f m = Q(m)`, this is the canonical lift of `f` to a morphism of `R`-algebras
 from `clifford_algebra Q` to `A`.
@@ -132,21 +143,27 @@ def lift : { f : M →ₗ[R] A // ∀ m, f m * f m = algebraMap _ _ (Q m) } ≃
       LinearMap.coe_comp, Subtype.coe_mk, RingQuot.liftAlgHom_mkAlgHom_apply,
       TensorAlgebra.lift_ι_apply]
 #align clifford_algebra.lift CliffordAlgebra.lift
+-/
 
 variable {Q}
 
+#print CliffordAlgebra.ι_comp_lift /-
 @[simp]
 theorem ι_comp_lift (f : M →ₗ[R] A) (cond : ∀ m, f m * f m = algebraMap _ _ (Q m)) :
     (lift Q ⟨f, cond⟩).toLinearMap.comp (ι Q) = f :=
   Subtype.mk_eq_mk.mp <| (lift Q).symm_apply_apply ⟨f, cond⟩
 #align clifford_algebra.ι_comp_lift CliffordAlgebra.ι_comp_lift
+-/
 
+#print CliffordAlgebra.lift_ι_apply /-
 @[simp]
 theorem lift_ι_apply (f : M →ₗ[R] A) (cond : ∀ m, f m * f m = algebraMap _ _ (Q m)) (x) :
     lift Q ⟨f, cond⟩ (ι Q x) = f x :=
   (LinearMap.ext_iff.mp <| ι_comp_lift f cond) x
 #align clifford_algebra.lift_ι_apply CliffordAlgebra.lift_ι_apply
+-/
 
+#print CliffordAlgebra.lift_unique /-
 @[simp]
 theorem lift_unique (f : M →ₗ[R] A) (cond : ∀ m : M, f m * f m = algebraMap _ _ (Q m))
     (g : CliffordAlgebra Q →ₐ[R] A) : g.toLinearMap.comp (ι Q) = f ↔ g = lift Q ⟨f, cond⟩ :=
@@ -155,7 +172,9 @@ theorem lift_unique (f : M →ₗ[R] A) (cond : ∀ m : M, f m * f m = algebraMa
   rw [lift_symm_apply]
   simp only
 #align clifford_algebra.lift_unique CliffordAlgebra.lift_unique
+-/
 
+#print CliffordAlgebra.lift_comp_ι /-
 @[simp]
 theorem lift_comp_ι (g : CliffordAlgebra Q →ₐ[R] A) :
     lift Q ⟨g.toLinearMap.comp (ι Q), comp_ι_sq_scalar _⟩ = g :=
@@ -164,7 +183,9 @@ theorem lift_comp_ι (g : CliffordAlgebra Q →ₐ[R] A) :
   rw [lift_symm_apply]
   rfl
 #align clifford_algebra.lift_comp_ι CliffordAlgebra.lift_comp_ι
+-/
 
+#print CliffordAlgebra.hom_ext /-
 /-- See note [partially-applied ext lemmas]. -/
 @[ext]
 theorem hom_ext {A : Type _} [Semiring A] [Algebra R A] {f g : CliffordAlgebra Q →ₐ[R] A} :
@@ -175,7 +196,9 @@ theorem hom_ext {A : Type _} [Semiring A] [Algebra R A] {f g : CliffordAlgebra Q
   rw [lift_symm_apply, lift_symm_apply]
   simp only [h]
 #align clifford_algebra.hom_ext CliffordAlgebra.hom_ext
+-/
 
+#print CliffordAlgebra.induction /-
 -- This proof closely follows `tensor_algebra.induction`
 /-- If `C` holds for the `algebra_map` of `r : R` into `clifford_algebra Q`, the `ι` of `x : M`,
 and is preserved under addition and muliplication, then it holds for all of `clifford_algebra Q`.
@@ -205,7 +228,9 @@ theorem induction {C : CliffordAlgebra Q → Prop}
   convert Subtype.prop (lift Q of a)
   exact AlgHom.congr_fun of_id a
 #align clifford_algebra.induction CliffordAlgebra.induction
+-/
 
+#print CliffordAlgebra.ι_mul_ι_add_swap /-
 /-- The symmetric product of vectors is a scalar -/
 theorem ι_mul_ι_add_swap (a b : M) :
     ι Q a * ι Q b + ι Q b * ι Q a = algebraMap R _ (QuadraticForm.polar Q a b) :=
@@ -217,24 +242,31 @@ theorem ι_mul_ι_add_swap (a b : M) :
     _ = algebraMap R _ (Q (a + b) - Q a - Q b) := by rw [← RingHom.map_sub, ← RingHom.map_sub]
     _ = algebraMap R _ (QuadraticForm.polar Q a b) := rfl
 #align clifford_algebra.ι_mul_ι_add_swap CliffordAlgebra.ι_mul_ι_add_swap
+-/
 
+#print CliffordAlgebra.ι_mul_comm /-
 theorem ι_mul_comm (a b : M) :
     ι Q a * ι Q b = algebraMap R _ (QuadraticForm.polar Q a b) - ι Q b * ι Q a :=
   eq_sub_of_add_eq (ι_mul_ι_add_swap a b)
 #align clifford_algebra.ι_mul_comm CliffordAlgebra.ι_mul_comm
+-/
 
+#print CliffordAlgebra.ι_mul_ι_mul_ι /-
 /-- $aba$ is a vector. -/
 theorem ι_mul_ι_mul_ι (a b : M) :
     ι Q a * ι Q b * ι Q a = ι Q (QuadraticForm.polar Q a b • a - Q a • b) := by
   rw [ι_mul_comm, sub_mul, mul_assoc, ι_sq_scalar, ← Algebra.smul_def, ← Algebra.commutes, ←
     Algebra.smul_def, ← map_smul, ← map_smul, ← map_sub]
 #align clifford_algebra.ι_mul_ι_mul_ι CliffordAlgebra.ι_mul_ι_mul_ι
+-/
 
+#print CliffordAlgebra.ι_range_map_lift /-
 @[simp]
 theorem ι_range_map_lift (f : M →ₗ[R] A) (cond : ∀ m, f m * f m = algebraMap _ _ (Q m)) :
     (ι Q).range.map (lift Q ⟨f, cond⟩).toLinearMap = f.range := by
   rw [← LinearMap.range_comp, ι_comp_lift]
 #align clifford_algebra.ι_range_map_lift CliffordAlgebra.ι_range_map_lift
+-/
 
 section Map
 
@@ -246,6 +278,7 @@ variable [Module R M₁] [Module R M₂] [Module R M₃]
 
 variable (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) (Q₃ : QuadraticForm R M₃)
 
+#print CliffordAlgebra.map /-
 /-- Any linear map that preserves the quadratic form lifts to an `alg_hom` between algebras.
 
 See `clifford_algebra.equiv_of_isometry` for the case when `f` is a `quadratic_form.isometry`. -/
@@ -254,24 +287,32 @@ def map (f : M₁ →ₗ[R] M₂) (hf : ∀ m, Q₂ (f m) = Q₁ m) :
   CliffordAlgebra.lift Q₁
     ⟨(CliffordAlgebra.ι Q₂).comp f, fun m => (ι_sq_scalar _ _).trans <| RingHom.congr_arg _ <| hf m⟩
 #align clifford_algebra.map CliffordAlgebra.map
+-/
 
+#print CliffordAlgebra.map_comp_ι /-
 @[simp]
 theorem map_comp_ι (f : M₁ →ₗ[R] M₂) (hf) :
     (map Q₁ Q₂ f hf).toLinearMap.comp (ι Q₁) = (ι Q₂).comp f :=
   ι_comp_lift _ _
 #align clifford_algebra.map_comp_ι CliffordAlgebra.map_comp_ι
+-/
 
+#print CliffordAlgebra.map_apply_ι /-
 @[simp]
 theorem map_apply_ι (f : M₁ →ₗ[R] M₂) (hf) (m : M₁) : map Q₁ Q₂ f hf (ι Q₁ m) = ι Q₂ (f m) :=
   lift_ι_apply _ _ m
 #align clifford_algebra.map_apply_ι CliffordAlgebra.map_apply_ι
+-/
 
+#print CliffordAlgebra.map_id /-
 @[simp]
 theorem map_id :
     (map Q₁ Q₁ (LinearMap.id : M₁ →ₗ[R] M₁) fun m => rfl) = AlgHom.id R (CliffordAlgebra Q₁) := by
   ext m; exact map_apply_ι _ _ _ _ m
 #align clifford_algebra.map_id CliffordAlgebra.map_id
+-/
 
+#print CliffordAlgebra.map_comp_map /-
 @[simp]
 theorem map_comp_map (f : M₂ →ₗ[R] M₃) (hf) (g : M₁ →ₗ[R] M₂) (hg) :
     (map Q₂ Q₃ f hf).comp (map Q₁ Q₂ g hg) = map Q₁ Q₃ (f.comp g) fun m => (hf _).trans <| hg m :=
@@ -280,15 +321,19 @@ theorem map_comp_map (f : M₂ →ₗ[R] M₃) (hf) (g : M₁ →ₗ[R] M₂) (h
   dsimp only [LinearMap.comp_apply, AlgHom.comp_apply, AlgHom.toLinearMap_apply, AlgHom.id_apply]
   rw [map_apply_ι, map_apply_ι, map_apply_ι, LinearMap.comp_apply]
 #align clifford_algebra.map_comp_map CliffordAlgebra.map_comp_map
+-/
 
+#print CliffordAlgebra.ι_range_map_map /-
 @[simp]
 theorem ι_range_map_map (f : M₁ →ₗ[R] M₂) (hf : ∀ m, Q₂ (f m) = Q₁ m) :
     (ι Q₁).range.map (map Q₁ Q₂ f hf).toLinearMap = f.range.map (ι Q₂) :=
   (ι_range_map_lift _ _).trans (LinearMap.range_comp _ _)
 #align clifford_algebra.ι_range_map_map CliffordAlgebra.ι_range_map_map
+-/
 
 variable {Q₁ Q₂ Q₃}
 
+#print CliffordAlgebra.equivOfIsometry /-
 /-- Two `clifford_algebra`s are equivalent as algebras if their quadratic forms are
 equivalent. -/
 @[simps apply]
@@ -305,29 +350,37 @@ def equivOfIsometry (e : Q₁.Isometry Q₂) : CliffordAlgebra Q₁ ≃ₐ[R] Cl
       ext m
       exact e.to_linear_equiv.symm_apply_apply m)
 #align clifford_algebra.equiv_of_isometry CliffordAlgebra.equivOfIsometry
+-/
 
+#print CliffordAlgebra.equivOfIsometry_symm /-
 @[simp]
 theorem equivOfIsometry_symm (e : Q₁.Isometry Q₂) :
     (equivOfIsometry e).symm = equivOfIsometry e.symm :=
   rfl
 #align clifford_algebra.equiv_of_isometry_symm CliffordAlgebra.equivOfIsometry_symm
+-/
 
+#print CliffordAlgebra.equivOfIsometry_trans /-
 @[simp]
 theorem equivOfIsometry_trans (e₁₂ : Q₁.Isometry Q₂) (e₂₃ : Q₂.Isometry Q₃) :
     (equivOfIsometry e₁₂).trans (equivOfIsometry e₂₃) = equivOfIsometry (e₁₂.trans e₂₃) := by ext x;
   exact AlgHom.congr_fun (map_comp_map Q₁ Q₂ Q₃ _ _ _ _) x
 #align clifford_algebra.equiv_of_isometry_trans CliffordAlgebra.equivOfIsometry_trans
+-/
 
+#print CliffordAlgebra.equivOfIsometry_refl /-
 @[simp]
 theorem equivOfIsometry_refl :
     (equivOfIsometry <| QuadraticForm.Isometry.refl Q₁) = AlgEquiv.refl := by ext x;
   exact AlgHom.congr_fun (map_id Q₁) x
 #align clifford_algebra.equiv_of_isometry_refl CliffordAlgebra.equivOfIsometry_refl
+-/
 
 end Map
 
 variable (Q)
 
+#print CliffordAlgebra.invertibleιOfInvertible /-
 /-- If the quadratic form of a vector is invertible, then so is that vector. -/
 def invertibleιOfInvertible (m : M) [Invertible (Q m)] : Invertible (ι Q m)
     where
@@ -337,51 +390,64 @@ def invertibleιOfInvertible (m : M) [Invertible (Q m)] : Invertible (ι Q m)
   mul_invOf_self := by
     rw [map_smul, mul_smul_comm, ι_sq_scalar, Algebra.smul_def, ← map_mul, invOf_mul_self, map_one]
 #align clifford_algebra.invertible_ι_of_invertible CliffordAlgebra.invertibleιOfInvertible
+-/
 
+#print CliffordAlgebra.invOf_ι /-
 /-- For a vector with invertible quadratic form, $v^{-1} = \frac{v}{Q(v)}$ -/
 theorem invOf_ι (m : M) [Invertible (Q m)] [Invertible (ι Q m)] : ⅟ (ι Q m) = ι Q (⅟ (Q m) • m) :=
   by
   letI := invertible_ι_of_invertible Q m
   convert (rfl : ⅟ (ι Q m) = _)
 #align clifford_algebra.inv_of_ι CliffordAlgebra.invOf_ι
+-/
 
+#print CliffordAlgebra.isUnit_ι_of_isUnit /-
 theorem isUnit_ι_of_isUnit {m : M} (h : IsUnit (Q m)) : IsUnit (ι Q m) :=
   by
   cases h.nonempty_invertible
   letI := invertible_ι_of_invertible Q m
   exact isUnit_of_invertible (ι Q m)
 #align clifford_algebra.is_unit_ι_of_is_unit CliffordAlgebra.isUnit_ι_of_isUnit
+-/
 
+#print CliffordAlgebra.ι_mul_ι_mul_invOf_ι /-
 /-- $aba^{-1}$ is a vector. -/
 theorem ι_mul_ι_mul_invOf_ι (a b : M) [Invertible (ι Q a)] [Invertible (Q a)] :
     ι Q a * ι Q b * ⅟ (ι Q a) = ι Q ((⅟ (Q a) * QuadraticForm.polar Q a b) • a - b) := by
   rw [inv_of_ι, map_smul, mul_smul_comm, ι_mul_ι_mul_ι, ← map_smul, smul_sub, smul_smul, smul_smul,
     invOf_mul_self, one_smul]
 #align clifford_algebra.ι_mul_ι_mul_inv_of_ι CliffordAlgebra.ι_mul_ι_mul_invOf_ι
+-/
 
+#print CliffordAlgebra.invOf_ι_mul_ι_mul_ι /-
 /-- $a^{-1}ba$ is a vector. -/
 theorem invOf_ι_mul_ι_mul_ι (a b : M) [Invertible (ι Q a)] [Invertible (Q a)] :
     ⅟ (ι Q a) * ι Q b * ι Q a = ι Q ((⅟ (Q a) * QuadraticForm.polar Q a b) • a - b) := by
   rw [inv_of_ι, map_smul, smul_mul_assoc, smul_mul_assoc, ι_mul_ι_mul_ι, ← map_smul, smul_sub,
     smul_smul, smul_smul, invOf_mul_self, one_smul]
 #align clifford_algebra.inv_of_ι_mul_ι_mul_ι CliffordAlgebra.invOf_ι_mul_ι_mul_ι
+-/
 
 end CliffordAlgebra
 
 namespace TensorAlgebra
 
 variable {Q}
 
+#print TensorAlgebra.toClifford /-
 /-- The canonical image of the `tensor_algebra` in the `clifford_algebra`, which maps
 `tensor_algebra.ι R x` to `clifford_algebra.ι Q x`. -/
 def toClifford : TensorAlgebra R M →ₐ[R] CliffordAlgebra Q :=
   TensorAlgebra.lift R (CliffordAlgebra.ι Q)
 #align tensor_algebra.to_clifford TensorAlgebra.toClifford
+-/
 
+#print TensorAlgebra.toClifford_ι /-
 @[simp]
 theorem toClifford_ι (m : M) : (TensorAlgebra.ι R m).toClifford = CliffordAlgebra.ι Q m := by
   simp [to_clifford]
 #align tensor_algebra.to_clifford_ι TensorAlgebra.toClifford_ι
+-/
 
 end TensorAlgebra
 

Mathbin/LinearAlgebra/CliffordAlgebra/Equivs.lean

@@ -81,7 +81,7 @@ theorem ι_eq_zero : ι (0 : QuadraticForm R Unit) = 0 :=
 
 /-- Since the vector space is empty the ring is commutative. -/
 instance : CommRing (CliffordAlgebra (0 : QuadraticForm R Unit)) :=
-  { CliffordAlgebra.ring _ with
+  { CliffordAlgebra.instRing _ with
     mul_comm := fun x y => by
       induction x using CliffordAlgebra.induction
       case h_grade0 r => apply Algebra.commutes
@@ -216,7 +216,7 @@ protected def equiv : CliffordAlgebra q ≃ₐ[ℝ] ℂ :=
 
 TODO: prove this is true for all `clifford_algebra`s over a 1-dimensional vector space. -/
 instance : CommRing (CliffordAlgebra q) :=
-  { CliffordAlgebra.ring _ with
+  { CliffordAlgebra.instRing _ with
     mul_comm := fun x y =>
       CliffordAlgebraComplex.equiv.Injective <| by
         rw [AlgEquiv.map_mul, mul_comm, AlgEquiv.map_mul] }

Mathbin/LinearAlgebra/PiTensorProduct.lean

@@ -259,21 +259,21 @@ variable [Monoid R₁] [DistribMulAction R₁ R] [SMulCommClass R₁ R R]
 
 variable [Monoid R₂] [DistribMulAction R₂ R] [SMulCommClass R₂ R R]
 
-#print PiTensorProduct.hasSmul' /-
+#print PiTensorProduct.hasSMul' /-
 -- Most of the time we want the instance below this one, which is easier for typeclass resolution
 -- to find.
-instance hasSmul' : SMul R₁ (⨂[R] i, s i) :=
+instance hasSMul' : SMul R₁ (⨂[R] i, s i) :=
   ⟨fun r =>
     liftAddHom (fun f : R × ∀ i, s i => tprodCoeff R (r • f.1) f.2)
       (fun r' f i hf => by simp_rw [zero_tprod_coeff' _ f i hf])
       (fun f => by simp [zero_tprod_coeff]) (fun r' f i m₁ m₂ => by simp [add_tprod_coeff])
       (fun r' r'' f => by simp [add_tprod_coeff', mul_add]) fun z f i r' => by
       simp [smul_tprod_coeff, mul_smul_comm]⟩
-#align pi_tensor_product.has_smul' PiTensorProduct.hasSmul'
+#align pi_tensor_product.has_smul' PiTensorProduct.hasSMul'
 -/
 
 instance : SMul R (⨂[R] i, s i) :=
-  PiTensorProduct.hasSmul'
+  PiTensorProduct.hasSMul'
 
 #print PiTensorProduct.smul_tprodCoeff' /-
 theorem smul_tprodCoeff' (r : R₁) (z : R) (f : ∀ i, s i) :