Skip to content

Commit

Permalink
bump to nightly-2023-05-18-01
Browse files Browse the repository at this point in the history 
mathlib commit leanprover-community/mathlib@f8c79b0
  • Loading branch information
@leanprover-community-bot
leanprover-community-bot committed May 18, 2023
1 parent 761032a commit 932bf4e
Show file tree
Hide file tree
Showing 6 changed files with 572 additions and 20 deletions.
42 changes: 42 additions & 0 deletions Mathbin/Analysis/NormedSpace/IsROrC.lean
View file

Large diffs are not rendered by default.

452 changes: 452 additions & 0 deletions Mathbin/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
View file

Large diffs are not rendered by default.

12 changes: 12 additions & 0 deletions Mathbin/LinearAlgebra/Multilinear/FiniteDimensional.lean
View file
Expand Up @@ -71,10 +71,22 @@ private theorem free_and_finite :
exact ⟨Module.Free.linearMap _ _ _, Module.Finite.linearMap _ _⟩
#align multilinear_map.free_and_finite multilinear_map.free_and_finite

/- warning: module.finite.multilinear_map -> Module.Finite.multilinearMap is a dubious translation:
lean 3 declaration is
forall {ι : Type.{u1}} {R : Type.{u2}} {M₂ : Type.{u3}} {M₁ : ι -> Type.{u4}} [_inst_1 : Finite.{succ u1} ι] [_inst_2 : CommRing.{u2} R] [_inst_3 : AddCommGroup.{u3} M₂] [_inst_4 : Module.{u2, u3} R M₂ (Ring.toSemiring.{u2} R (CommRing.toRing.{u2} R _inst_2)) (AddCommGroup.toAddCommMonoid.{u3} M₂ _inst_3)] [_inst_5 : forall (i : ι), AddCommGroup.{u4} (M₁ i)] [_inst_6 : forall (i : ι), Module.{u2, u4} R (M₁ i) (Ring.toSemiring.{u2} R (CommRing.toRing.{u2} R _inst_2)) (AddCommGroup.toAddCommMonoid.{u4} (M₁ i) (_inst_5 i))] [_inst_7 : Module.Finite.{u2, u3} R M₂ (Ring.toSemiring.{u2} R (CommRing.toRing.{u2} R _inst_2)) (AddCommGroup.toAddCommMonoid.{u3} M₂ _inst_3) _inst_4] [_inst_8 : Module.Free.{u2, u3} R M₂ (Ring.toSemiring.{u2} R (CommRing.toRing.{u2} R _inst_2)) (AddCommGroup.toAddCommMonoid.{u3} M₂ _inst_3) _inst_4] [_inst_9 : forall (i : ι), Module.Finite.{u2, u4} R (M₁ i) (Ring.toSemiring.{u2} R (CommRing.toRing.{u2} R _inst_2)) (AddCommGroup.toAddCommMonoid.{u4} (M₁ i) (_inst_5 i)) (_inst_6 i)] [_inst_10 : forall (i : ι), Module.Free.{u2, u4} R (M₁ i) (Ring.toSemiring.{u2} R (CommRing.toRing.{u2} R _inst_2)) (AddCommGroup.toAddCommMonoid.{u4} (M₁ i) (_inst_5 i)) (_inst_6 i)], Module.Finite.{u2, max u1 u4 u3} R (MultilinearMap.{u2, u4, u3, u1} R ι M₁ M₂ (Ring.toSemiring.{u2} R (CommRing.toRing.{u2} R _inst_2)) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u4} (M₁ i) (_inst_5 i)) (AddCommGroup.toAddCommMonoid.{u3} M₂ _inst_3) (fun (i : ι) => _inst_6 i) _inst_4) (Ring.toSemiring.{u2} R (CommRing.toRing.{u2} R _inst_2)) (MultilinearMap.addCommMonoid.{u2, u4, u3, u1} R ι M₁ M₂ (Ring.toSemiring.{u2} R (CommRing.toRing.{u2} R _inst_2)) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u4} (M₁ i) (_inst_5 i)) (AddCommGroup.toAddCommMonoid.{u3} M₂ _inst_3) (fun (i : ι) => _inst_6 i) _inst_4) (MultilinearMap.module.{u4, u3, u1, u2, u2} ι M₁ M₂ (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u4} (M₁ i) (_inst_5 i)) (AddCommGroup.toAddCommMonoid.{u3} M₂ _inst_3) R R (Ring.toSemiring.{u2} R (CommRing.toRing.{u2} R _inst_2)) (Ring.toSemiring.{u2} R (CommRing.toRing.{u2} R _inst_2)) (fun (i : ι) => _inst_6 i) _inst_4 _inst_4 (smulCommClass_self.{u2, u3} R M₂ (CommRing.toCommMonoid.{u2} R _inst_2) (MulActionWithZero.toMulAction.{u2, u3} R M₂ (Semiring.toMonoidWithZero.{u2} R (Ring.toSemiring.{u2} R (CommRing.toRing.{u2} R _inst_2))) (AddZeroClass.toHasZero.{u3} M₂ (AddMonoid.toAddZeroClass.{u3} M₂ (AddCommMonoid.toAddMonoid.{u3} M₂ (AddCommGroup.toAddCommMonoid.{u3} M₂ _inst_3)))) (Module.toMulActionWithZero.{u2, u3} R M₂ (Ring.toSemiring.{u2} R (CommRing.toRing.{u2} R _inst_2)) (AddCommGroup.toAddCommMonoid.{u3} M₂ _inst_3) _inst_4))))
but is expected to have type
forall {ι : Type.{u1}} {R : Type.{u2}} {M₂ : Type.{u3}} {M₁ : ι -> Type.{u4}} [_inst_1 : Finite.{succ u1} ι] [_inst_2 : CommRing.{u2} R] [_inst_3 : AddCommGroup.{u3} M₂] [_inst_4 : Module.{u2, u3} R M₂ (CommSemiring.toSemiring.{u2} R (CommRing.toCommSemiring.{u2} R _inst_2)) (AddCommGroup.toAddCommMonoid.{u3} M₂ _inst_3)] [_inst_5 : Module.Finite.{u2, u3} R M₂ (CommSemiring.toSemiring.{u2} R (CommRing.toCommSemiring.{u2} R _inst_2)) (AddCommGroup.toAddCommMonoid.{u3} M₂ _inst_3) _inst_4] [_inst_6 : Module.Free.{u2, u3} R M₂ (CommSemiring.toSemiring.{u2} R (CommRing.toCommSemiring.{u2} R _inst_2)) (AddCommGroup.toAddCommMonoid.{u3} M₂ _inst_3) _inst_4] [_inst_7 : forall (i : ι), AddCommGroup.{u4} (M₁ i)] [_inst_8 : forall (i : ι), Module.{u2, u4} R (M₁ i) (CommSemiring.toSemiring.{u2} R (CommRing.toCommSemiring.{u2} R _inst_2)) (AddCommGroup.toAddCommMonoid.{u4} (M₁ i) (_inst_7 i))] [_inst_9 : forall (i : ι), Module.Finite.{u2, u4} R (M₁ i) (CommSemiring.toSemiring.{u2} R (CommRing.toCommSemiring.{u2} R _inst_2)) (AddCommGroup.toAddCommMonoid.{u4} (M₁ i) (_inst_7 i)) (_inst_8 i)] [_inst_10 : forall (i : ι), Module.Free.{u2, u4} R (M₁ i) (CommSemiring.toSemiring.{u2} R (CommRing.toCommSemiring.{u2} R _inst_2)) (AddCommGroup.toAddCommMonoid.{u4} (M₁ i) (_inst_7 i)) (_inst_8 i)], Module.Finite.{u2, max (max u1 u3) u4} R (MultilinearMap.{u2, u4, u3, u1} R ι M₁ M₂ (CommSemiring.toSemiring.{u2} R (CommRing.toCommSemiring.{u2} R _inst_2)) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u4} (M₁ i) (_inst_7 i)) (AddCommGroup.toAddCommMonoid.{u3} M₂ _inst_3) (fun (i : ι) => _inst_8 i) _inst_4) (CommSemiring.toSemiring.{u2} R (CommRing.toCommSemiring.{u2} R _inst_2)) (MultilinearMap.addCommMonoid.{u2, u4, u3, u1} R ι M₁ M₂ (CommSemiring.toSemiring.{u2} R (CommRing.toCommSemiring.{u2} R _inst_2)) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u4} (M₁ i) (_inst_7 i)) (AddCommGroup.toAddCommMonoid.{u3} M₂ _inst_3) (fun (i : ι) => _inst_8 i) _inst_4) (MultilinearMap.instModuleMultilinearMapAddCommMonoid.{u4, u3, u1, u2, u2} ι M₁ M₂ (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u4} (M₁ i) (_inst_7 i)) (AddCommGroup.toAddCommMonoid.{u3} M₂ _inst_3) R R (CommSemiring.toSemiring.{u2} R (CommRing.toCommSemiring.{u2} R _inst_2)) (CommSemiring.toSemiring.{u2} R (CommRing.toCommSemiring.{u2} R _inst_2)) (fun (i : ι) => _inst_8 i) _inst_4 _inst_4 (smulCommClass_self.{u2, u3} R M₂ (CommRing.toCommMonoid.{u2} R _inst_2) (MulActionWithZero.toMulAction.{u2, u3} R M₂ (Semiring.toMonoidWithZero.{u2} R (CommSemiring.toSemiring.{u2} R (CommRing.toCommSemiring.{u2} R _inst_2))) (NegZeroClass.toZero.{u3} M₂ (SubNegZeroMonoid.toNegZeroClass.{u3} M₂ (SubtractionMonoid.toSubNegZeroMonoid.{u3} M₂ (SubtractionCommMonoid.toSubtractionMonoid.{u3} M₂ (AddCommGroup.toDivisionAddCommMonoid.{u3} M₂ _inst_3))))) (Module.toMulActionWithZero.{u2, u3} R M₂ (CommSemiring.toSemiring.{u2} R (CommRing.toCommSemiring.{u2} R _inst_2)) (AddCommGroup.toAddCommMonoid.{u3} M₂ _inst_3) _inst_4))))
Case conversion may be inaccurate. Consider using '#align module.finite.multilinear_map Module.Finite.multilinearMapₓ'. -/
instance Module.Finite.multilinearMap : Module.Finite R (MultilinearMap R M₁ M₂) :=
free_and_finite.2
#align module.finite.multilinear_map Module.Finite.multilinearMap

/- warning: module.free.multilinear_map -> Module.Free.multilinearMap is a dubious translation:
lean 3 declaration is
forall {ι : Type.{u1}} {R : Type.{u2}} {M₂ : Type.{u3}} {M₁ : ι -> Type.{u4}} [_inst_1 : Finite.{succ u1} ι] [_inst_2 : CommRing.{u2} R] [_inst_3 : AddCommGroup.{u3} M₂] [_inst_4 : Module.{u2, u3} R M₂ (Ring.toSemiring.{u2} R (CommRing.toRing.{u2} R _inst_2)) (AddCommGroup.toAddCommMonoid.{u3} M₂ _inst_3)] [_inst_5 : forall (i : ι), AddCommGroup.{u4} (M₁ i)] [_inst_6 : forall (i : ι), Module.{u2, u4} R (M₁ i) (Ring.toSemiring.{u2} R (CommRing.toRing.{u2} R _inst_2)) (AddCommGroup.toAddCommMonoid.{u4} (M₁ i) (_inst_5 i))] [_inst_7 : Module.Finite.{u2, u3} R M₂ (Ring.toSemiring.{u2} R (CommRing.toRing.{u2} R _inst_2)) (AddCommGroup.toAddCommMonoid.{u3} M₂ _inst_3) _inst_4] [_inst_8 : Module.Free.{u2, u3} R M₂ (Ring.toSemiring.{u2} R (CommRing.toRing.{u2} R _inst_2)) (AddCommGroup.toAddCommMonoid.{u3} M₂ _inst_3) _inst_4] [_inst_9 : forall (i : ι), Module.Finite.{u2, u4} R (M₁ i) (Ring.toSemiring.{u2} R (CommRing.toRing.{u2} R _inst_2)) (AddCommGroup.toAddCommMonoid.{u4} (M₁ i) (_inst_5 i)) (_inst_6 i)] [_inst_10 : forall (i : ι), Module.Free.{u2, u4} R (M₁ i) (Ring.toSemiring.{u2} R (CommRing.toRing.{u2} R _inst_2)) (AddCommGroup.toAddCommMonoid.{u4} (M₁ i) (_inst_5 i)) (_inst_6 i)], Module.Free.{u2, max u1 u4 u3} R (MultilinearMap.{u2, u4, u3, u1} R ι M₁ M₂ (Ring.toSemiring.{u2} R (CommRing.toRing.{u2} R _inst_2)) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u4} (M₁ i) (_inst_5 i)) (AddCommGroup.toAddCommMonoid.{u3} M₂ _inst_3) (fun (i : ι) => _inst_6 i) _inst_4) (Ring.toSemiring.{u2} R (CommRing.toRing.{u2} R _inst_2)) (MultilinearMap.addCommMonoid.{u2, u4, u3, u1} R ι M₁ M₂ (Ring.toSemiring.{u2} R (CommRing.toRing.{u2} R _inst_2)) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u4} (M₁ i) (_inst_5 i)) (AddCommGroup.toAddCommMonoid.{u3} M₂ _inst_3) (fun (i : ι) => _inst_6 i) _inst_4) (MultilinearMap.module.{u4, u3, u1, u2, u2} ι M₁ M₂ (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u4} (M₁ i) (_inst_5 i)) (AddCommGroup.toAddCommMonoid.{u3} M₂ _inst_3) R R (Ring.toSemiring.{u2} R (CommRing.toRing.{u2} R _inst_2)) (Ring.toSemiring.{u2} R (CommRing.toRing.{u2} R _inst_2)) (fun (i : ι) => _inst_6 i) _inst_4 _inst_4 (smulCommClass_self.{u2, u3} R M₂ (CommRing.toCommMonoid.{u2} R _inst_2) (MulActionWithZero.toMulAction.{u2, u3} R M₂ (Semiring.toMonoidWithZero.{u2} R (Ring.toSemiring.{u2} R (CommRing.toRing.{u2} R _inst_2))) (AddZeroClass.toHasZero.{u3} M₂ (AddMonoid.toAddZeroClass.{u3} M₂ (AddCommMonoid.toAddMonoid.{u3} M₂ (AddCommGroup.toAddCommMonoid.{u3} M₂ _inst_3)))) (Module.toMulActionWithZero.{u2, u3} R M₂ (Ring.toSemiring.{u2} R (CommRing.toRing.{u2} R _inst_2)) (AddCommGroup.toAddCommMonoid.{u3} M₂ _inst_3) _inst_4))))
but is expected to have type
forall {ι : Type.{u1}} {R : Type.{u2}} {M₂ : Type.{u3}} {M₁ : ι -> Type.{u4}} [_inst_1 : Finite.{succ u1} ι] [_inst_2 : CommRing.{u2} R] [_inst_3 : AddCommGroup.{u3} M₂] [_inst_4 : Module.{u2, u3} R M₂ (CommSemiring.toSemiring.{u2} R (CommRing.toCommSemiring.{u2} R _inst_2)) (AddCommGroup.toAddCommMonoid.{u3} M₂ _inst_3)] [_inst_5 : Module.Finite.{u2, u3} R M₂ (CommSemiring.toSemiring.{u2} R (CommRing.toCommSemiring.{u2} R _inst_2)) (AddCommGroup.toAddCommMonoid.{u3} M₂ _inst_3) _inst_4] [_inst_6 : Module.Free.{u2, u3} R M₂ (CommSemiring.toSemiring.{u2} R (CommRing.toCommSemiring.{u2} R _inst_2)) (AddCommGroup.toAddCommMonoid.{u3} M₂ _inst_3) _inst_4] [_inst_7 : forall (i : ι), AddCommGroup.{u4} (M₁ i)] [_inst_8 : forall (i : ι), Module.{u2, u4} R (M₁ i) (CommSemiring.toSemiring.{u2} R (CommRing.toCommSemiring.{u2} R _inst_2)) (AddCommGroup.toAddCommMonoid.{u4} (M₁ i) (_inst_7 i))] [_inst_9 : forall (i : ι), Module.Finite.{u2, u4} R (M₁ i) (CommSemiring.toSemiring.{u2} R (CommRing.toCommSemiring.{u2} R _inst_2)) (AddCommGroup.toAddCommMonoid.{u4} (M₁ i) (_inst_7 i)) (_inst_8 i)] [_inst_10 : forall (i : ι), Module.Free.{u2, u4} R (M₁ i) (CommSemiring.toSemiring.{u2} R (CommRing.toCommSemiring.{u2} R _inst_2)) (AddCommGroup.toAddCommMonoid.{u4} (M₁ i) (_inst_7 i)) (_inst_8 i)], Module.Free.{u2, max (max u1 u3) u4} R (MultilinearMap.{u2, u4, u3, u1} R ι M₁ M₂ (CommSemiring.toSemiring.{u2} R (CommRing.toCommSemiring.{u2} R _inst_2)) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u4} (M₁ i) (_inst_7 i)) (AddCommGroup.toAddCommMonoid.{u3} M₂ _inst_3) (fun (i : ι) => _inst_8 i) _inst_4) (CommSemiring.toSemiring.{u2} R (CommRing.toCommSemiring.{u2} R _inst_2)) (MultilinearMap.addCommMonoid.{u2, u4, u3, u1} R ι M₁ M₂ (CommSemiring.toSemiring.{u2} R (CommRing.toCommSemiring.{u2} R _inst_2)) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u4} (M₁ i) (_inst_7 i)) (AddCommGroup.toAddCommMonoid.{u3} M₂ _inst_3) (fun (i : ι) => _inst_8 i) _inst_4) (MultilinearMap.instModuleMultilinearMapAddCommMonoid.{u4, u3, u1, u2, u2} ι M₁ M₂ (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u4} (M₁ i) (_inst_7 i)) (AddCommGroup.toAddCommMonoid.{u3} M₂ _inst_3) R R (CommSemiring.toSemiring.{u2} R (CommRing.toCommSemiring.{u2} R _inst_2)) (CommSemiring.toSemiring.{u2} R (CommRing.toCommSemiring.{u2} R _inst_2)) (fun (i : ι) => _inst_8 i) _inst_4 _inst_4 (smulCommClass_self.{u2, u3} R M₂ (CommRing.toCommMonoid.{u2} R _inst_2) (MulActionWithZero.toMulAction.{u2, u3} R M₂ (Semiring.toMonoidWithZero.{u2} R (CommSemiring.toSemiring.{u2} R (CommRing.toCommSemiring.{u2} R _inst_2))) (NegZeroClass.toZero.{u3} M₂ (SubNegZeroMonoid.toNegZeroClass.{u3} M₂ (SubtractionMonoid.toSubNegZeroMonoid.{u3} M₂ (SubtractionCommMonoid.toSubtractionMonoid.{u3} M₂ (AddCommGroup.toDivisionAddCommMonoid.{u3} M₂ _inst_3))))) (Module.toMulActionWithZero.{u2, u3} R M₂ (CommSemiring.toSemiring.{u2} R (CommRing.toCommSemiring.{u2} R _inst_2)) (AddCommGroup.toAddCommMonoid.{u3} M₂ _inst_3) _inst_4))))
Case conversion may be inaccurate. Consider using '#align module.free.multilinear_map Module.Free.multilinearMapₓ'. -/
instance Module.Free.multilinearMap : Module.Free R (MultilinearMap R M₁ M₂) :=
free_and_finite.1
#align module.free.multilinear_map Module.Free.multilinearMap
Expand Down
74 changes: 60 additions & 14 deletions Mathbin/RingTheory/Polynomial/Quotient.lean
View file

Large diffs are not rendered by default.

8 changes: 4 additions & 4 deletions lake-manifest.json
View file
Expand Up @@ -4,15 +4,15 @@
[{"git":
{"url": "https://github.com/leanprover-community/lean3port.git",
"subDir?": null,
"rev": "bbacb93e5ae354a37554f53bce1c5e45a88a8561",
"rev": "d0b0ac50adf565935d153470bc0fa23833eaa21e",
"name": "lean3port",
"inputRev?": "bbacb93e5ae354a37554f53bce1c5e45a88a8561"}},
"inputRev?": "d0b0ac50adf565935d153470bc0fa23833eaa21e"}},
{"git":
{"url": "https://github.com/leanprover-community/mathlib4.git",
"subDir?": null,
"rev": "9ab4016508c1a4590481a1b548db651937bf2e04",
"rev": "d0c30e109e20aba2015a60de85b0c0d0412a4d5d",
"name": "mathlib",
"inputRev?": "9ab4016508c1a4590481a1b548db651937bf2e04"}},
"inputRev?": "d0c30e109e20aba2015a60de85b0c0d0412a4d5d"}},
{"git":
{"url": "https://github.com/gebner/quote4",
"subDir?": null,
Expand Down
4 changes: 2 additions & 2 deletions lakefile.lean
View file
Expand Up @@ -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-05-17-22"
def tag : String := "nightly-2023-05-18-01"
def releaseRepo : String := "leanprover-community/mathport"
def oleanTarName : String := "mathlib3-binport.tar.gz"

Expand Down Expand Up @@ -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"@"bbacb93e5ae354a37554f53bce1c5e45a88a8561"
require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"d0b0ac50adf565935d153470bc0fa23833eaa21e"

@[default_target]
lean_lib Mathbin where
Expand Down

0 comments on commit 932bf4e

Please sign in to comment.