From 4fed16d53f4486f1042235378b7e5ee9b3c0de61 Mon Sep 17 00:00:00 2001 From: leanprover-community-bot Date: Fri, 24 Mar 2023 14:40:26 +0000 Subject: [PATCH] bump to nightly-2023-03-24-14 mathlib commit https://github.com/leanprover-community/mathlib/commit/b19481deb571022990f1baa9cbf9172e6757a479 --- Mathbin/Algebra/Star/Free.lean | 30 +++++ Mathbin/NumberTheory/Fermat4.lean | 56 ++++++++ Mathbin/NumberTheory/Padics/PadicNorm.lean | 146 +++++++++++++++++++++ lake-manifest.json | 8 +- lakefile.lean | 4 +- 5 files changed, 238 insertions(+), 6 deletions(-) diff --git a/Mathbin/Algebra/Star/Free.lean b/Mathbin/Algebra/Star/Free.lean index 8084acedc3..2bd6662ae3 100644 --- a/Mathbin/Algebra/Star/Free.lean +++ b/Mathbin/Algebra/Star/Free.lean @@ -32,11 +32,23 @@ instance : StarSemigroup (FreeMonoid α) star_involutive := List.reverse_reverse star_mul := List.reverse_append +/- warning: free_monoid.star_of -> FreeMonoid.star_of is a dubious translation: +lean 3 declaration is + forall {α : Type.{u1}} (x : α), Eq.{succ u1} (FreeMonoid.{u1} α) (Star.star.{u1} (FreeMonoid.{u1} α) (InvolutiveStar.toHasStar.{u1} (FreeMonoid.{u1} α) (StarSemigroup.toHasInvolutiveStar.{u1} (FreeMonoid.{u1} α) (Monoid.toSemigroup.{u1} (FreeMonoid.{u1} α) (RightCancelMonoid.toMonoid.{u1} (FreeMonoid.{u1} α) (CancelMonoid.toRightCancelMonoid.{u1} (FreeMonoid.{u1} α) (FreeMonoid.cancelMonoid.{u1} α)))) (FreeMonoid.starSemigroup.{u1} α))) (FreeMonoid.of.{u1} α x)) (FreeMonoid.of.{u1} α x) +but is expected to have type + forall {α : Type.{u1}} (x : α), Eq.{succ u1} (FreeMonoid.{u1} α) (Star.star.{u1} (FreeMonoid.{u1} α) (InvolutiveStar.toStar.{u1} (FreeMonoid.{u1} α) (StarSemigroup.toInvolutiveStar.{u1} (FreeMonoid.{u1} α) (Monoid.toSemigroup.{u1} (FreeMonoid.{u1} α) (RightCancelMonoid.toMonoid.{u1} (FreeMonoid.{u1} α) (CancelMonoid.toRightCancelMonoid.{u1} (FreeMonoid.{u1} α) (FreeMonoid.instCancelMonoidFreeMonoid.{u1} α)))) (FreeMonoid.instStarSemigroupFreeMonoidToSemigroupToMonoidToRightCancelMonoidInstCancelMonoidFreeMonoid.{u1} α))) (FreeMonoid.of.{u1} α x)) (FreeMonoid.of.{u1} α x) +Case conversion may be inaccurate. Consider using '#align free_monoid.star_of FreeMonoid.star_ofₓ'. -/ @[simp] theorem star_of (x : α) : star (of x) = of x := rfl #align free_monoid.star_of FreeMonoid.star_of +/- warning: free_monoid.star_one -> FreeMonoid.star_one is a dubious translation: +lean 3 declaration is + forall {α : Type.{u1}}, Eq.{succ u1} (FreeMonoid.{u1} α) (Star.star.{u1} (FreeMonoid.{u1} α) (InvolutiveStar.toHasStar.{u1} (FreeMonoid.{u1} α) (StarSemigroup.toHasInvolutiveStar.{u1} (FreeMonoid.{u1} α) (Monoid.toSemigroup.{u1} (FreeMonoid.{u1} α) (RightCancelMonoid.toMonoid.{u1} (FreeMonoid.{u1} α) (CancelMonoid.toRightCancelMonoid.{u1} (FreeMonoid.{u1} α) (FreeMonoid.cancelMonoid.{u1} α)))) (FreeMonoid.starSemigroup.{u1} α))) (OfNat.ofNat.{u1} (FreeMonoid.{u1} α) 1 (OfNat.mk.{u1} (FreeMonoid.{u1} α) 1 (One.one.{u1} (FreeMonoid.{u1} α) (MulOneClass.toHasOne.{u1} (FreeMonoid.{u1} α) (Monoid.toMulOneClass.{u1} (FreeMonoid.{u1} α) (RightCancelMonoid.toMonoid.{u1} (FreeMonoid.{u1} α) (CancelMonoid.toRightCancelMonoid.{u1} (FreeMonoid.{u1} α) (FreeMonoid.cancelMonoid.{u1} α))))))))) (OfNat.ofNat.{u1} (FreeMonoid.{u1} α) 1 (OfNat.mk.{u1} (FreeMonoid.{u1} α) 1 (One.one.{u1} (FreeMonoid.{u1} α) (MulOneClass.toHasOne.{u1} (FreeMonoid.{u1} α) (Monoid.toMulOneClass.{u1} (FreeMonoid.{u1} α) (RightCancelMonoid.toMonoid.{u1} (FreeMonoid.{u1} α) (CancelMonoid.toRightCancelMonoid.{u1} (FreeMonoid.{u1} α) (FreeMonoid.cancelMonoid.{u1} α)))))))) +but is expected to have type + forall {α : Type.{u1}}, Eq.{succ u1} (FreeMonoid.{u1} α) (Star.star.{u1} (FreeMonoid.{u1} α) (InvolutiveStar.toStar.{u1} (FreeMonoid.{u1} α) (StarSemigroup.toInvolutiveStar.{u1} (FreeMonoid.{u1} α) (Monoid.toSemigroup.{u1} (FreeMonoid.{u1} α) (RightCancelMonoid.toMonoid.{u1} (FreeMonoid.{u1} α) (CancelMonoid.toRightCancelMonoid.{u1} (FreeMonoid.{u1} α) (FreeMonoid.instCancelMonoidFreeMonoid.{u1} α)))) (FreeMonoid.instStarSemigroupFreeMonoidToSemigroupToMonoidToRightCancelMonoidInstCancelMonoidFreeMonoid.{u1} α))) (OfNat.ofNat.{u1} (FreeMonoid.{u1} α) 1 (One.toOfNat1.{u1} (FreeMonoid.{u1} α) (RightCancelMonoid.toOne.{u1} (FreeMonoid.{u1} α) (CancelMonoid.toRightCancelMonoid.{u1} (FreeMonoid.{u1} α) (FreeMonoid.instCancelMonoidFreeMonoid.{u1} α)))))) (OfNat.ofNat.{u1} (FreeMonoid.{u1} α) 1 (One.toOfNat1.{u1} (FreeMonoid.{u1} α) (RightCancelMonoid.toOne.{u1} (FreeMonoid.{u1} α) (CancelMonoid.toRightCancelMonoid.{u1} (FreeMonoid.{u1} α) (FreeMonoid.instCancelMonoidFreeMonoid.{u1} α))))) +Case conversion may be inaccurate. Consider using '#align free_monoid.star_one FreeMonoid.star_oneₓ'. -/ /-- Note that `star_one` is already a global simp lemma, but this one works with dsimp too -/ @[simp] theorem star_one : star (1 : FreeMonoid α) = 1 := @@ -68,15 +80,33 @@ instance : StarRing (FreeAlgebra R X) star_mul a b := by simp only [Function.comp_apply, map_mul, MulOpposite.unop_mul] star_add a b := by simp only [Function.comp_apply, map_add, MulOpposite.unop_add] +/- warning: free_algebra.star_ι -> FreeAlgebra.star_ι is a dubious translation: +lean 3 declaration is + forall {R : Type.{u1}} [_inst_1 : CommSemiring.{u1} R] {X : Type.{u2}} (x : X), Eq.{succ (max u1 u2)} (FreeAlgebra.{u1, u2} R _inst_1 X) (Star.star.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (InvolutiveStar.toHasStar.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (StarAddMonoid.toHasInvolutiveStar.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (AddCommMonoid.toAddMonoid.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (NonUnitalNonAssocSemiring.toAddCommMonoid.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (NonUnitalSemiring.toNonUnitalNonAssocSemiring.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (Semiring.toNonUnitalSemiring.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (FreeAlgebra.semiring.{u1, u2} R _inst_1 X))))) (StarRing.toStarAddMonoid.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (Semiring.toNonUnitalSemiring.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (FreeAlgebra.semiring.{u1, u2} R _inst_1 X)) (FreeAlgebra.starRing.{u1, u2} R _inst_1 X)))) (FreeAlgebra.ι.{u1, u2} R _inst_1 X x)) (FreeAlgebra.ι.{u1, u2} R _inst_1 X x) +but is expected to have type + forall {R : Type.{u2}} [_inst_1 : CommSemiring.{u2} R] {X : Type.{u1}} (x : X), Eq.{max (succ u2) (succ u1)} (FreeAlgebra.{u2, u1} R _inst_1 X) (Star.star.{max u2 u1} (FreeAlgebra.{u2, u1} R _inst_1 X) (InvolutiveStar.toStar.{max u2 u1} (FreeAlgebra.{u2, u1} R _inst_1 X) (StarAddMonoid.toInvolutiveStar.{max u2 u1} (FreeAlgebra.{u2, u1} R _inst_1 X) (AddMonoidWithOne.toAddMonoid.{max u2 u1} (FreeAlgebra.{u2, u1} R _inst_1 X) (AddCommMonoidWithOne.toAddMonoidWithOne.{max u2 u1} (FreeAlgebra.{u2, u1} R _inst_1 X) (NonAssocSemiring.toAddCommMonoidWithOne.{max u2 u1} (FreeAlgebra.{u2, u1} R _inst_1 X) (Semiring.toNonAssocSemiring.{max u2 u1} (FreeAlgebra.{u2, u1} R _inst_1 X) (FreeAlgebra.instSemiringFreeAlgebra.{u2, u1} R _inst_1 X))))) (StarRing.toStarAddMonoid.{max u2 u1} (FreeAlgebra.{u2, u1} R _inst_1 X) (Semiring.toNonUnitalSemiring.{max u2 u1} (FreeAlgebra.{u2, u1} R _inst_1 X) (FreeAlgebra.instSemiringFreeAlgebra.{u2, u1} R _inst_1 X)) (FreeAlgebra.instStarRingFreeAlgebraToNonUnitalSemiringInstSemiringFreeAlgebra.{u2, u1} R _inst_1 X)))) (FreeAlgebra.ι.{u2, u1} R _inst_1 X x)) (FreeAlgebra.ι.{u2, u1} R _inst_1 X x) +Case conversion may be inaccurate. Consider using '#align free_algebra.star_ι FreeAlgebra.star_ιₓ'. -/ @[simp] theorem star_ι (x : X) : star (ι R x) = ι R x := by simp [star, Star.star] #align free_algebra.star_ι FreeAlgebra.star_ι +/- warning: free_algebra.star_algebra_map -> FreeAlgebra.star_algebraMap is a dubious translation: +lean 3 declaration is + forall {R : Type.{u1}} [_inst_1 : CommSemiring.{u1} R] {X : Type.{u2}} (r : R), Eq.{succ (max u1 u2)} (FreeAlgebra.{u1, u2} R _inst_1 X) (Star.star.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (InvolutiveStar.toHasStar.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (StarAddMonoid.toHasInvolutiveStar.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (AddCommMonoid.toAddMonoid.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (NonUnitalNonAssocSemiring.toAddCommMonoid.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (NonUnitalSemiring.toNonUnitalNonAssocSemiring.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (Semiring.toNonUnitalSemiring.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (FreeAlgebra.semiring.{u1, u2} R _inst_1 X))))) (StarRing.toStarAddMonoid.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (Semiring.toNonUnitalSemiring.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (FreeAlgebra.semiring.{u1, u2} R _inst_1 X)) (FreeAlgebra.starRing.{u1, u2} R _inst_1 X)))) (coeFn.{max (succ u1) (succ (max u1 u2)), max (succ u1) (succ (max u1 u2))} (RingHom.{u1, max u1 u2} R (FreeAlgebra.{u1, u2} R _inst_1 X) (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (FreeAlgebra.semiring.{u1, u2} R _inst_1 X))) (fun (_x : RingHom.{u1, max u1 u2} R (FreeAlgebra.{u1, u2} R _inst_1 X) (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (FreeAlgebra.semiring.{u1, u2} R _inst_1 X))) => R -> (FreeAlgebra.{u1, u2} R _inst_1 X)) (RingHom.hasCoeToFun.{u1, max u1 u2} R (FreeAlgebra.{u1, u2} R _inst_1 X) (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (FreeAlgebra.semiring.{u1, u2} R _inst_1 X))) (algebraMap.{u1, max u1 u2} R (FreeAlgebra.{u1, u2} R _inst_1 X) _inst_1 (FreeAlgebra.semiring.{u1, u2} R _inst_1 X) (FreeAlgebra.algebra.{u1, u2} R _inst_1 X)) r)) (coeFn.{max (succ u1) (succ (max u1 u2)), max (succ u1) (succ (max u1 u2))} (RingHom.{u1, max u1 u2} R (FreeAlgebra.{u1, u2} R _inst_1 X) (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (FreeAlgebra.semiring.{u1, u2} R _inst_1 X))) (fun (_x : RingHom.{u1, max u1 u2} R (FreeAlgebra.{u1, u2} R _inst_1 X) (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (FreeAlgebra.semiring.{u1, u2} R _inst_1 X))) => R -> (FreeAlgebra.{u1, u2} R _inst_1 X)) (RingHom.hasCoeToFun.{u1, max u1 u2} R (FreeAlgebra.{u1, u2} R _inst_1 X) (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (FreeAlgebra.semiring.{u1, u2} R _inst_1 X))) (algebraMap.{u1, max u1 u2} R (FreeAlgebra.{u1, u2} R _inst_1 X) _inst_1 (FreeAlgebra.semiring.{u1, u2} R _inst_1 X) (FreeAlgebra.algebra.{u1, u2} R _inst_1 X)) r) +but is expected to have type + forall {R : Type.{u2}} [_inst_1 : CommSemiring.{u2} R] {X : Type.{u1}} (r : R), Eq.{max (succ u2) (succ u1)} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => FreeAlgebra.{u2, u1} R _inst_1 X) r) (Star.star.{max u2 u1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => FreeAlgebra.{u2, u1} R _inst_1 X) r) (InvolutiveStar.toStar.{max u2 u1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => FreeAlgebra.{u2, u1} R _inst_1 X) r) (StarAddMonoid.toInvolutiveStar.{max u2 u1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => FreeAlgebra.{u2, u1} R _inst_1 X) r) (AddMonoidWithOne.toAddMonoid.{max u2 u1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => FreeAlgebra.{u2, u1} R _inst_1 X) r) (AddCommMonoidWithOne.toAddMonoidWithOne.{max u2 u1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => FreeAlgebra.{u2, u1} R _inst_1 X) r) (NonAssocSemiring.toAddCommMonoidWithOne.{max u2 u1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => FreeAlgebra.{u2, u1} R _inst_1 X) r) (Semiring.toNonAssocSemiring.{max u2 u1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => FreeAlgebra.{u2, u1} R _inst_1 X) r) (FreeAlgebra.instSemiringFreeAlgebra.{u2, u1} R _inst_1 X))))) (StarRing.toStarAddMonoid.{max u2 u1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => FreeAlgebra.{u2, u1} R _inst_1 X) r) (Semiring.toNonUnitalSemiring.{max u2 u1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => FreeAlgebra.{u2, u1} R _inst_1 X) r) (FreeAlgebra.instSemiringFreeAlgebra.{u2, u1} R _inst_1 X)) (FreeAlgebra.instStarRingFreeAlgebraToNonUnitalSemiringInstSemiringFreeAlgebra.{u2, u1} R _inst_1 X)))) (FunLike.coe.{max (succ u2) (succ u1), succ u2, max (succ u2) (succ u1)} (RingHom.{u2, max u1 u2} R (FreeAlgebra.{u2, u1} R _inst_1 X) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{max u1 u2} (FreeAlgebra.{u2, u1} R _inst_1 X) (FreeAlgebra.instSemiringFreeAlgebra.{u2, u1} R _inst_1 X))) R (fun (_x : R) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => FreeAlgebra.{u2, u1} R _inst_1 X) _x) (MulHomClass.toFunLike.{max u2 u1, u2, max u2 u1} (RingHom.{u2, max u1 u2} R (FreeAlgebra.{u2, u1} R _inst_1 X) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{max u1 u2} (FreeAlgebra.{u2, u1} R _inst_1 X) (FreeAlgebra.instSemiringFreeAlgebra.{u2, u1} R _inst_1 X))) R (FreeAlgebra.{u2, u1} R _inst_1 X) (NonUnitalNonAssocSemiring.toMul.{u2} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} R (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)))) (NonUnitalNonAssocSemiring.toMul.{max u2 u1} (FreeAlgebra.{u2, u1} R _inst_1 X) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{max u2 u1} (FreeAlgebra.{u2, u1} R _inst_1 X) (Semiring.toNonAssocSemiring.{max u1 u2} (FreeAlgebra.{u2, u1} R _inst_1 X) (FreeAlgebra.instSemiringFreeAlgebra.{u2, u1} R _inst_1 X)))) (NonUnitalRingHomClass.toMulHomClass.{max u2 u1, u2, max u2 u1} (RingHom.{u2, max u1 u2} R (FreeAlgebra.{u2, u1} R _inst_1 X) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{max u1 u2} (FreeAlgebra.{u2, u1} R _inst_1 X) (FreeAlgebra.instSemiringFreeAlgebra.{u2, u1} R _inst_1 X))) R (FreeAlgebra.{u2, u1} R _inst_1 X) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} R (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{max u2 u1} (FreeAlgebra.{u2, u1} R _inst_1 X) (Semiring.toNonAssocSemiring.{max u1 u2} (FreeAlgebra.{u2, u1} R _inst_1 X) (FreeAlgebra.instSemiringFreeAlgebra.{u2, u1} R _inst_1 X))) (RingHomClass.toNonUnitalRingHomClass.{max u2 u1, u2, max u2 u1} (RingHom.{u2, max u1 u2} R (FreeAlgebra.{u2, u1} R _inst_1 X) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{max u1 u2} (FreeAlgebra.{u2, u1} R _inst_1 X) (FreeAlgebra.instSemiringFreeAlgebra.{u2, u1} R _inst_1 X))) R (FreeAlgebra.{u2, u1} R _inst_1 X) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{max u1 u2} (FreeAlgebra.{u2, u1} R _inst_1 X) (FreeAlgebra.instSemiringFreeAlgebra.{u2, u1} R _inst_1 X)) (RingHom.instRingHomClassRingHom.{u2, max u2 u1} R (FreeAlgebra.{u2, u1} R _inst_1 X) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{max u1 u2} (FreeAlgebra.{u2, u1} R _inst_1 X) (FreeAlgebra.instSemiringFreeAlgebra.{u2, u1} R _inst_1 X)))))) (algebraMap.{u2, max u1 u2} R (FreeAlgebra.{u2, u1} R _inst_1 X) _inst_1 (FreeAlgebra.instSemiringFreeAlgebra.{u2, u1} R _inst_1 X) (FreeAlgebra.instAlgebraFreeAlgebraInstSemiringFreeAlgebra.{u2, u1} R _inst_1 X)) r)) (FunLike.coe.{max (succ u2) (succ (max u2 u1)), succ u2, succ (max u2 u1)} (RingHom.{u2, max u2 u1} R (FreeAlgebra.{u2, u1} R _inst_1 X) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{max u2 u1} (FreeAlgebra.{u2, u1} R _inst_1 X) (FreeAlgebra.instSemiringFreeAlgebra.{u2, u1} R _inst_1 X))) R (fun (_x : R) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => FreeAlgebra.{u2, u1} R _inst_1 X) _x) (MulHomClass.toFunLike.{max u2 u1, u2, max u2 u1} (RingHom.{u2, max u2 u1} R (FreeAlgebra.{u2, u1} R _inst_1 X) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{max u2 u1} (FreeAlgebra.{u2, u1} R _inst_1 X) (FreeAlgebra.instSemiringFreeAlgebra.{u2, u1} R _inst_1 X))) R (FreeAlgebra.{u2, u1} R _inst_1 X) (NonUnitalNonAssocSemiring.toMul.{u2} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} R (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)))) (NonUnitalNonAssocSemiring.toMul.{max u2 u1} (FreeAlgebra.{u2, u1} R _inst_1 X) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{max u2 u1} (FreeAlgebra.{u2, u1} R _inst_1 X) (Semiring.toNonAssocSemiring.{max u2 u1} (FreeAlgebra.{u2, u1} R _inst_1 X) (FreeAlgebra.instSemiringFreeAlgebra.{u2, u1} R _inst_1 X)))) (NonUnitalRingHomClass.toMulHomClass.{max u2 u1, u2, max u2 u1} (RingHom.{u2, max u2 u1} R (FreeAlgebra.{u2, u1} R _inst_1 X) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{max u2 u1} (FreeAlgebra.{u2, u1} R _inst_1 X) (FreeAlgebra.instSemiringFreeAlgebra.{u2, u1} R _inst_1 X))) R (FreeAlgebra.{u2, u1} R _inst_1 X) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} R (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{max u2 u1} (FreeAlgebra.{u2, u1} R _inst_1 X) (Semiring.toNonAssocSemiring.{max u2 u1} (FreeAlgebra.{u2, u1} R _inst_1 X) (FreeAlgebra.instSemiringFreeAlgebra.{u2, u1} R _inst_1 X))) (RingHomClass.toNonUnitalRingHomClass.{max u2 u1, u2, max u2 u1} (RingHom.{u2, max u2 u1} R (FreeAlgebra.{u2, u1} R _inst_1 X) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{max u2 u1} (FreeAlgebra.{u2, u1} R _inst_1 X) (FreeAlgebra.instSemiringFreeAlgebra.{u2, u1} R _inst_1 X))) R (FreeAlgebra.{u2, u1} R _inst_1 X) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{max u2 u1} (FreeAlgebra.{u2, u1} R _inst_1 X) (FreeAlgebra.instSemiringFreeAlgebra.{u2, u1} R _inst_1 X)) (RingHom.instRingHomClassRingHom.{u2, max u2 u1} R (FreeAlgebra.{u2, u1} R _inst_1 X) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{max u2 u1} (FreeAlgebra.{u2, u1} R _inst_1 X) (FreeAlgebra.instSemiringFreeAlgebra.{u2, u1} R _inst_1 X)))))) (algebraMap.{u2, max u2 u1} R (FreeAlgebra.{u2, u1} R _inst_1 X) _inst_1 (FreeAlgebra.instSemiringFreeAlgebra.{u2, u1} R _inst_1 X) (FreeAlgebra.instAlgebraFreeAlgebraInstSemiringFreeAlgebra.{u2, u1} R _inst_1 X)) r) +Case conversion may be inaccurate. Consider using '#align free_algebra.star_algebra_map FreeAlgebra.star_algebraMapₓ'. -/ @[simp] theorem star_algebraMap (r : R) : star (algebraMap R (FreeAlgebra R X) r) = algebraMap R _ r := by simp [star, Star.star] #align free_algebra.star_algebra_map FreeAlgebra.star_algebraMap +/- warning: free_algebra.star_hom -> FreeAlgebra.starHom is a dubious translation: +lean 3 declaration is + forall {R : Type.{u1}} [_inst_1 : CommSemiring.{u1} R] {X : Type.{u2}}, AlgEquiv.{u1, max u1 u2, max u1 u2} R (FreeAlgebra.{u1, u2} R _inst_1 X) (MulOpposite.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X)) _inst_1 (FreeAlgebra.semiring.{u1, u2} R _inst_1 X) (MulOpposite.semiring.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (FreeAlgebra.semiring.{u1, u2} R _inst_1 X)) (FreeAlgebra.algebra.{u1, u2} R _inst_1 X) (MulOpposite.algebra.{u1, max u1 u2} R (FreeAlgebra.{u1, u2} R _inst_1 X) _inst_1 (FreeAlgebra.semiring.{u1, u2} R _inst_1 X) (FreeAlgebra.algebra.{u1, u2} R _inst_1 X)) +but is expected to have type + forall {R : Type.{u1}} [_inst_1 : CommSemiring.{u1} R] {X : Type.{u2}}, AlgEquiv.{u1, max u2 u1, max u2 u1} R (FreeAlgebra.{u1, u2} R _inst_1 X) (MulOpposite.{max u2 u1} (FreeAlgebra.{u1, u2} R _inst_1 X)) _inst_1 (FreeAlgebra.instSemiringFreeAlgebra.{u1, u2} R _inst_1 X) (MulOpposite.instSemiringMulOpposite.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (FreeAlgebra.instSemiringFreeAlgebra.{u1, u2} R _inst_1 X)) (FreeAlgebra.instAlgebraFreeAlgebraInstSemiringFreeAlgebra.{u1, u2} R _inst_1 X) (MulOpposite.instAlgebraMulOppositeInstSemiringMulOpposite.{u1, max u1 u2} R (FreeAlgebra.{u1, u2} R _inst_1 X) _inst_1 (FreeAlgebra.instSemiringFreeAlgebra.{u1, u2} R _inst_1 X) (FreeAlgebra.instAlgebraFreeAlgebraInstSemiringFreeAlgebra.{u1, u2} R _inst_1 X)) +Case conversion may be inaccurate. Consider using '#align free_algebra.star_hom FreeAlgebra.starHomₓ'. -/ /-- `star` as an `alg_equiv` -/ def starHom : FreeAlgebra R X ≃ₐ[R] (FreeAlgebra R X)ᵐᵒᵖ := { starRingEquiv with commutes' := fun r => by simp [star_algebra_map] } diff --git a/Mathbin/NumberTheory/Fermat4.lean b/Mathbin/NumberTheory/Fermat4.lean index 005ab061af..49bf15238b 100644 --- a/Mathbin/NumberTheory/Fermat4.lean +++ b/Mathbin/NumberTheory/Fermat4.lean @@ -22,22 +22,32 @@ noncomputable section open Classical +#print Fermat42 /- /-- Shorthand for three non-zero integers `a`, `b`, and `c` satisfying `a ^ 4 + b ^ 4 = c ^ 2`. We will show that no integers satisfy this equation. Clearly Fermat's Last theorem for n = 4 follows. -/ def Fermat42 (a b c : ℤ) : Prop := a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2 #align fermat_42 Fermat42 +-/ namespace Fermat42 +#print Fermat42.comm /- theorem comm {a b c : ℤ} : Fermat42 a b c ↔ Fermat42 b a c := by delta Fermat42 rw [add_comm] tauto #align fermat_42.comm Fermat42.comm +-/ +/- warning: fermat_42.mul -> Fermat42.mul is a dubious translation: +lean 3 declaration is + forall {a : Int} {b : Int} {c : Int} {k : Int}, (Ne.{1} Int k (OfNat.ofNat.{0} Int 0 (OfNat.mk.{0} Int 0 (Zero.zero.{0} Int Int.hasZero)))) -> (Iff (Fermat42 a b c) (Fermat42 (HMul.hMul.{0, 0, 0} Int Int Int (instHMul.{0} Int Int.hasMul) k a) (HMul.hMul.{0, 0, 0} Int Int Int (instHMul.{0} Int Int.hasMul) k b) (HMul.hMul.{0, 0, 0} Int Int Int (instHMul.{0} Int Int.hasMul) (HPow.hPow.{0, 0, 0} Int Nat Int (instHPow.{0, 0} Int Nat (Monoid.Pow.{0} Int Int.monoid)) k (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))))) c))) +but is expected to have type + forall {a : Int} {b : Int} {c : Int} {k : Int}, (Ne.{1} Int k (OfNat.ofNat.{0} Int 0 (instOfNatInt 0))) -> (Iff (Fermat42 a b c) (Fermat42 (HMul.hMul.{0, 0, 0} Int Int Int (instHMul.{0} Int Int.instMulInt) k a) (HMul.hMul.{0, 0, 0} Int Int Int (instHMul.{0} Int Int.instMulInt) k b) (HMul.hMul.{0, 0, 0} Int Int Int (instHMul.{0} Int Int.instMulInt) (HPow.hPow.{0, 0, 0} Int Nat Int (instHPow.{0, 0} Int Nat (Monoid.Pow.{0} Int Int.instMonoidInt)) k (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) c))) +Case conversion may be inaccurate. Consider using '#align fermat_42.mul Fermat42.mulₓ'. -/ theorem mul {a b c k : ℤ} (hk0 : k ≠ 0) : Fermat42 a b c ↔ Fermat42 (k * a) (k * b) (k ^ 2 * c) := by delta Fermat42 @@ -58,6 +68,7 @@ theorem mul {a b c k : ℤ} (hk0 : k ≠ 0) : Fermat42 a b c ↔ Fermat42 (k * a linear_combination f42.2.2 #align fermat_42.mul Fermat42.mul +#print Fermat42.ne_zero /- theorem ne_zero {a b c : ℤ} (h : Fermat42 a b c) : c ≠ 0 := by apply ne_zero_pow two_ne_zero _; apply ne_of_gt @@ -65,13 +76,17 @@ theorem ne_zero {a b c : ℤ} (h : Fermat42 a b c) : c ≠ 0 := exact add_pos (sq_pos_of_ne_zero _ (pow_ne_zero 2 h.1)) (sq_pos_of_ne_zero _ (pow_ne_zero 2 h.2.1)) #align fermat_42.ne_zero Fermat42.ne_zero +-/ +#print Fermat42.Minimal /- /-- We say a solution to `a ^ 4 + b ^ 4 = c ^ 2` is minimal if there is no other solution with a smaller `c` (in absolute value). -/ def Minimal (a b c : ℤ) : Prop := Fermat42 a b c ∧ ∀ a1 b1 c1 : ℤ, Fermat42 a1 b1 c1 → Int.natAbs c ≤ Int.natAbs c1 #align fermat_42.minimal Fermat42.Minimal +-/ +#print Fermat42.exists_minimal /- /-- if we have a solution to `a ^ 4 + b ^ 4 = c ^ 2` then there must be a minimal one. -/ theorem exists_minimal {a b c : ℤ} (h : Fermat42 a b c) : ∃ a0 b0 c0, Minimal a0 b0 c0 := by @@ -91,7 +106,14 @@ theorem exists_minimal {a b c : ℤ} (h : Fermat42 a b c) : ∃ a0 b0 c0, Minima use ⟨a1, ⟨b1, c1⟩⟩ tauto #align fermat_42.exists_minimal Fermat42.exists_minimal +-/ +/- warning: fermat_42.coprime_of_minimal -> Fermat42.coprime_of_minimal is a dubious translation: +lean 3 declaration is + forall {a : Int} {b : Int} {c : Int}, (Fermat42.Minimal a b c) -> (IsCoprime.{0} Int Int.commSemiring a b) +but is expected to have type + forall {a : Int} {b : Int} {c : Int}, (Fermat42.Minimal a b c) -> (IsCoprime.{0} Int Int.instCommSemiringInt a b) +Case conversion may be inaccurate. Consider using '#align fermat_42.coprime_of_minimal Fermat42.coprime_of_minimalₓ'. -/ /-- a minimal solution to `a ^ 4 + b ^ 4 = c ^ 2` must have `a` and `b` coprime. -/ theorem coprime_of_minimal {a b c : ℤ} (h : Minimal a b c) : IsCoprime a b := by @@ -114,11 +136,14 @@ theorem coprime_of_minimal {a b c : ℤ} (h : Minimal a b c) : IsCoprime a b := · exact Nat.pos_of_ne_zero (Int.natAbs_ne_zero_of_ne_zero (NeZero hf)) #align fermat_42.coprime_of_minimal Fermat42.coprime_of_minimal +#print Fermat42.minimal_comm /- /-- We can swap `a` and `b` in a minimal solution to `a ^ 4 + b ^ 4 = c ^ 2`. -/ theorem minimal_comm {a b c : ℤ} : Minimal a b c → Minimal b a c := fun ⟨h1, h2⟩ => ⟨Fermat42.comm.mp h1, h2⟩ #align fermat_42.minimal_comm Fermat42.minimal_comm +-/ +#print Fermat42.neg_of_minimal /- /-- We can assume that a minimal solution to `a ^ 4 + b ^ 4 = c ^ 2` has positive `c`. -/ theorem neg_of_minimal {a b c : ℤ} : Minimal a b c → Minimal a b (-c) := by @@ -129,7 +154,9 @@ theorem neg_of_minimal {a b c : ℤ} : Minimal a b c → Minimal a b (-c) := exact (neg_sq c).symm rwa [Int.natAbs_neg c] #align fermat_42.neg_of_minimal Fermat42.neg_of_minimal +-/ +#print Fermat42.exists_odd_minimal /- /-- We can assume that a minimal solution to `a ^ 4 + b ^ 4 = c ^ 2` has `a` odd. -/ theorem exists_odd_minimal {a b c : ℤ} (h : Fermat42 a b c) : ∃ a0 b0 c0, Minimal a0 b0 c0 ∧ a0 % 2 = 1 := @@ -146,7 +173,9 @@ theorem exists_odd_minimal {a b c : ℤ} (h : Fermat42 a b c) : · exact ⟨b0, ⟨a0, ⟨c0, minimal_comm hf, hbp⟩⟩⟩ exact ⟨a0, ⟨b0, ⟨c0, hf, hap⟩⟩⟩ #align fermat_42.exists_odd_minimal Fermat42.exists_odd_minimal +-/ +#print Fermat42.exists_pos_odd_minimal /- /-- We can assume that a minimal solution to `a ^ 4 + b ^ 4 = c ^ 2` has `a` odd and `c` positive. -/ theorem exists_pos_odd_minimal {a b c : ℤ} (h : Fermat42 a b c) : @@ -161,15 +190,28 @@ theorem exists_pos_odd_minimal {a b c : ℤ} (h : Fermat42 a b c) : · use a0, b0, -c0, neg_of_minimal hf, hc exact neg_pos.mpr h1 #align fermat_42.exists_pos_odd_minimal Fermat42.exists_pos_odd_minimal +-/ end Fermat42 +/- warning: int.coprime_of_sq_sum -> Int.coprime_of_sq_sum is a dubious translation: +lean 3 declaration is + forall {r : Int} {s : Int}, (IsCoprime.{0} Int Int.commSemiring s r) -> (IsCoprime.{0} Int Int.commSemiring (HAdd.hAdd.{0, 0, 0} Int Int Int (instHAdd.{0} Int Int.hasAdd) (HPow.hPow.{0, 0, 0} Int Nat Int (instHPow.{0, 0} Int Nat (Monoid.Pow.{0} Int Int.monoid)) r (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))))) (HPow.hPow.{0, 0, 0} Int Nat Int (instHPow.{0, 0} Int Nat (Monoid.Pow.{0} Int Int.monoid)) s (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne)))))) r) +but is expected to have type + forall {r : Int} {s : Int}, (IsCoprime.{0} Int Int.instCommSemiringInt s r) -> (IsCoprime.{0} Int Int.instCommSemiringInt (HAdd.hAdd.{0, 0, 0} Int Int Int (instHAdd.{0} Int Int.instAddInt) (HPow.hPow.{0, 0, 0} Int Nat Int (instHPow.{0, 0} Int Nat (Monoid.Pow.{0} Int Int.instMonoidInt)) r (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) (HPow.hPow.{0, 0, 0} Int Nat Int (instHPow.{0, 0} Int Nat (Monoid.Pow.{0} Int Int.instMonoidInt)) s (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)))) r) +Case conversion may be inaccurate. Consider using '#align int.coprime_of_sq_sum Int.coprime_of_sq_sumₓ'. -/ theorem Int.coprime_of_sq_sum {r s : ℤ} (h2 : IsCoprime s r) : IsCoprime (r ^ 2 + s ^ 2) r := by rw [sq, sq] exact (IsCoprime.mul_left h2 h2).mul_add_left_left r #align int.coprime_of_sq_sum Int.coprime_of_sq_sum +/- warning: int.coprime_of_sq_sum' -> Int.coprime_of_sq_sum' is a dubious translation: +lean 3 declaration is + forall {r : Int} {s : Int}, (IsCoprime.{0} Int Int.commSemiring r s) -> (IsCoprime.{0} Int Int.commSemiring (HAdd.hAdd.{0, 0, 0} Int Int Int (instHAdd.{0} Int Int.hasAdd) (HPow.hPow.{0, 0, 0} Int Nat Int (instHPow.{0, 0} Int Nat (Monoid.Pow.{0} Int Int.monoid)) r (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))))) (HPow.hPow.{0, 0, 0} Int Nat Int (instHPow.{0, 0} Int Nat (Monoid.Pow.{0} Int Int.monoid)) s (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne)))))) (HMul.hMul.{0, 0, 0} Int Int Int (instHMul.{0} Int Int.hasMul) r s)) +but is expected to have type + forall {r : Int} {s : Int}, (IsCoprime.{0} Int Int.instCommSemiringInt r s) -> (IsCoprime.{0} Int Int.instCommSemiringInt (HAdd.hAdd.{0, 0, 0} Int Int Int (instHAdd.{0} Int Int.instAddInt) (HPow.hPow.{0, 0, 0} Int Nat Int (instHPow.{0, 0} Int Nat (Monoid.Pow.{0} Int Int.instMonoidInt)) r (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) (HPow.hPow.{0, 0, 0} Int Nat Int (instHPow.{0, 0} Int Nat (Monoid.Pow.{0} Int Int.instMonoidInt)) s (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)))) (HMul.hMul.{0, 0, 0} Int Int Int (instHMul.{0} Int Int.instMulInt) r s)) +Case conversion may be inaccurate. Consider using '#align int.coprime_of_sq_sum' Int.coprime_of_sq_sum'ₓ'. -/ theorem Int.coprime_of_sq_sum' {r s : ℤ} (h : IsCoprime r s) : IsCoprime (r ^ 2 + s ^ 2) (r * s) := by apply IsCoprime.mul_right (Int.coprime_of_sq_sum (is_coprime_comm.mp h)) @@ -178,6 +220,7 @@ theorem Int.coprime_of_sq_sum' {r s : ℤ} (h : IsCoprime r s) : IsCoprime (r ^ namespace Fermat42 +#print Fermat42.not_minimal /- -- If we have a solution to a ^ 4 + b ^ 4 = c ^ 2, we can construct a smaller one. This -- implies there can't be a smallest solution. theorem not_minimal {a b c : ℤ} (h : Minimal a b c) (ha2 : a % 2 = 1) (hc : 0 < c) : False := @@ -316,9 +359,16 @@ theorem not_minimal {a b c : ℤ} (h : Minimal a b c) (ha2 : a % 2 = 1) (hc : 0 exact ⟨hj0, hk0, hh.symm⟩ apply absurd (not_le_of_lt hic) (not_not.mpr hic') #align fermat_42.not_minimal Fermat42.not_minimal +-/ end Fermat42 +/- warning: not_fermat_42 -> not_fermat_42 is a dubious translation: +lean 3 declaration is + forall {a : Int} {b : Int} {c : Int}, (Ne.{1} Int a (OfNat.ofNat.{0} Int 0 (OfNat.mk.{0} Int 0 (Zero.zero.{0} Int Int.hasZero)))) -> (Ne.{1} Int b (OfNat.ofNat.{0} Int 0 (OfNat.mk.{0} Int 0 (Zero.zero.{0} Int Int.hasZero)))) -> (Ne.{1} Int (HAdd.hAdd.{0, 0, 0} Int Int Int (instHAdd.{0} Int Int.hasAdd) (HPow.hPow.{0, 0, 0} Int Nat Int (instHPow.{0, 0} Int Nat (Monoid.Pow.{0} Int Int.monoid)) a (OfNat.ofNat.{0} Nat 4 (OfNat.mk.{0} Nat 4 (bit0.{0} Nat Nat.hasAdd (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne)))))) (HPow.hPow.{0, 0, 0} Int Nat Int (instHPow.{0, 0} Int Nat (Monoid.Pow.{0} Int Int.monoid)) b (OfNat.ofNat.{0} Nat 4 (OfNat.mk.{0} Nat 4 (bit0.{0} Nat Nat.hasAdd (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))))))) (HPow.hPow.{0, 0, 0} Int Nat Int (instHPow.{0, 0} Int Nat (Monoid.Pow.{0} Int Int.monoid)) c (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne)))))) +but is expected to have type + forall {a : Int} {b : Int} {c : Int}, (Ne.{1} Int a (OfNat.ofNat.{0} Int 0 (instOfNatInt 0))) -> (Ne.{1} Int b (OfNat.ofNat.{0} Int 0 (instOfNatInt 0))) -> (Ne.{1} Int (HAdd.hAdd.{0, 0, 0} Int Int Int (instHAdd.{0} Int Int.instAddInt) (HPow.hPow.{0, 0, 0} Int Nat Int (instHPow.{0, 0} Int Nat (Monoid.Pow.{0} Int Int.instMonoidInt)) a (OfNat.ofNat.{0} Nat 4 (instOfNatNat 4))) (HPow.hPow.{0, 0, 0} Int Nat Int (instHPow.{0, 0} Int Nat (Monoid.Pow.{0} Int Int.instMonoidInt)) b (OfNat.ofNat.{0} Nat 4 (instOfNatNat 4)))) (HPow.hPow.{0, 0, 0} Int Nat Int (instHPow.{0, 0} Int Nat (Monoid.Pow.{0} Int Int.instMonoidInt)) c (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)))) +Case conversion may be inaccurate. Consider using '#align not_fermat_42 not_fermat_42ₓ'. -/ theorem not_fermat_42 {a b c : ℤ} (ha : a ≠ 0) (hb : b ≠ 0) : a ^ 4 + b ^ 4 ≠ c ^ 2 := by intro h @@ -327,6 +377,12 @@ theorem not_fermat_42 {a b c : ℤ} (ha : a ≠ 0) (hb : b ≠ 0) : a ^ 4 + b ^ apply Fermat42.not_minimal hf h2 hp #align not_fermat_42 not_fermat_42 +/- warning: not_fermat_4 -> not_fermat_4 is a dubious translation: +lean 3 declaration is + forall {a : Int} {b : Int} {c : Int}, (Ne.{1} Int a (OfNat.ofNat.{0} Int 0 (OfNat.mk.{0} Int 0 (Zero.zero.{0} Int Int.hasZero)))) -> (Ne.{1} Int b (OfNat.ofNat.{0} Int 0 (OfNat.mk.{0} Int 0 (Zero.zero.{0} Int Int.hasZero)))) -> (Ne.{1} Int (HAdd.hAdd.{0, 0, 0} Int Int Int (instHAdd.{0} Int Int.hasAdd) (HPow.hPow.{0, 0, 0} Int Nat Int (instHPow.{0, 0} Int Nat (Monoid.Pow.{0} Int Int.monoid)) a (OfNat.ofNat.{0} Nat 4 (OfNat.mk.{0} Nat 4 (bit0.{0} Nat Nat.hasAdd (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne)))))) (HPow.hPow.{0, 0, 0} Int Nat Int (instHPow.{0, 0} Int Nat (Monoid.Pow.{0} Int Int.monoid)) b (OfNat.ofNat.{0} Nat 4 (OfNat.mk.{0} Nat 4 (bit0.{0} Nat Nat.hasAdd (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))))))) (HPow.hPow.{0, 0, 0} Int Nat Int (instHPow.{0, 0} Int Nat (Monoid.Pow.{0} Int Int.monoid)) c (OfNat.ofNat.{0} Nat 4 (OfNat.mk.{0} Nat 4 (bit0.{0} Nat Nat.hasAdd (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))))))) +but is expected to have type + forall {a : Int} {b : Int} {c : Int}, (Ne.{1} Int a (OfNat.ofNat.{0} Int 0 (instOfNatInt 0))) -> (Ne.{1} Int b (OfNat.ofNat.{0} Int 0 (instOfNatInt 0))) -> (Ne.{1} Int (HAdd.hAdd.{0, 0, 0} Int Int Int (instHAdd.{0} Int Int.instAddInt) (HPow.hPow.{0, 0, 0} Int Nat Int (instHPow.{0, 0} Int Nat (Monoid.Pow.{0} Int Int.instMonoidInt)) a (OfNat.ofNat.{0} Nat 4 (instOfNatNat 4))) (HPow.hPow.{0, 0, 0} Int Nat Int (instHPow.{0, 0} Int Nat (Monoid.Pow.{0} Int Int.instMonoidInt)) b (OfNat.ofNat.{0} Nat 4 (instOfNatNat 4)))) (HPow.hPow.{0, 0, 0} Int Nat Int (instHPow.{0, 0} Int Nat (Monoid.Pow.{0} Int Int.instMonoidInt)) c (OfNat.ofNat.{0} Nat 4 (instOfNatNat 4)))) +Case conversion may be inaccurate. Consider using '#align not_fermat_4 not_fermat_4ₓ'. -/ theorem not_fermat_4 {a b c : ℤ} (ha : a ≠ 0) (hb : b ≠ 0) : a ^ 4 + b ^ 4 ≠ c ^ 4 := by intro heq diff --git a/Mathbin/NumberTheory/Padics/PadicNorm.lean b/Mathbin/NumberTheory/Padics/PadicNorm.lean index fe24106f2f..111388c090 100644 --- a/Mathbin/NumberTheory/Padics/PadicNorm.lean +++ b/Mathbin/NumberTheory/Padics/PadicNorm.lean @@ -43,11 +43,13 @@ p-adic, p adic, padic, norm, valuation -/ +#print padicNorm /- /-- If `q ≠ 0`, the `p`-adic norm of a rational `q` is `p ^ -padic_val_rat p q`. If `q = 0`, the `p`-adic norm of `q` is `0`. -/ def padicNorm (p : ℕ) (q : ℚ) : ℚ := if q = 0 then 0 else (p : ℚ) ^ (-padicValRat p q) #align padic_norm padicNorm +-/ namespace padicNorm @@ -55,12 +57,24 @@ open padicValRat variable {p : ℕ} +/- warning: padic_norm.eq_zpow_of_nonzero -> padicNorm.eq_zpow_of_nonzero is a dubious translation: +lean 3 declaration is + forall {p : Nat} {q : Rat}, (Ne.{1} Rat q (OfNat.ofNat.{0} Rat 0 (OfNat.mk.{0} Rat 0 (Zero.zero.{0} Rat Rat.hasZero)))) -> (Eq.{1} Rat (padicNorm p q) (HPow.hPow.{0, 0, 0} Rat Int Rat (instHPow.{0, 0} Rat Int (DivInvMonoid.Pow.{0} Rat (DivisionRing.toDivInvMonoid.{0} Rat Rat.divisionRing))) ((fun (a : Type) (b : Type) [self : HasLiftT.{1, 1} a b] => self.0) Nat Rat (HasLiftT.mk.{1, 1} Nat Rat (CoeTCₓ.coe.{1, 1} Nat Rat (Nat.castCoe.{0} Rat (AddMonoidWithOne.toNatCast.{0} Rat (AddGroupWithOne.toAddMonoidWithOne.{0} Rat (NonAssocRing.toAddGroupWithOne.{0} Rat (Ring.toNonAssocRing.{0} Rat (StrictOrderedRing.toRing.{0} Rat (LinearOrderedRing.toStrictOrderedRing.{0} Rat Rat.linearOrderedRing))))))))) p) (Neg.neg.{0} Int Int.hasNeg (padicValRat p q)))) +but is expected to have type + forall {p : Nat} {q : Rat}, (Ne.{1} Rat q (OfNat.ofNat.{0} Rat 0 (Rat.instOfNatRat 0))) -> (Eq.{1} Rat (padicNorm p q) (HPow.hPow.{0, 0, 0} Rat Int Rat (instHPow.{0, 0} Rat Int (DivInvMonoid.Pow.{0} Rat (DivisionRing.toDivInvMonoid.{0} Rat Rat.divisionRing))) (Nat.cast.{0} Rat (NonAssocRing.toNatCast.{0} Rat (Ring.toNonAssocRing.{0} Rat (DivisionRing.toRing.{0} Rat Rat.divisionRing))) p) (Neg.neg.{0} Int Int.instNegInt (padicValRat p q)))) +Case conversion may be inaccurate. Consider using '#align padic_norm.eq_zpow_of_nonzero padicNorm.eq_zpow_of_nonzeroₓ'. -/ /-- Unfolds the definition of the `p`-adic norm of `q` when `q ≠ 0`. -/ @[simp] protected theorem eq_zpow_of_nonzero {q : ℚ} (hq : q ≠ 0) : padicNorm p q = p ^ (-padicValRat p q) := by simp [hq, padicNorm] #align padic_norm.eq_zpow_of_nonzero padicNorm.eq_zpow_of_nonzero +/- warning: padic_norm.nonneg -> padicNorm.nonneg is a dubious translation: +lean 3 declaration is + forall {p : Nat} (q : Rat), LE.le.{0} Rat Rat.hasLe (OfNat.ofNat.{0} Rat 0 (OfNat.mk.{0} Rat 0 (Zero.zero.{0} Rat Rat.hasZero))) (padicNorm p q) +but is expected to have type + forall {p : Nat} (q : Rat), LE.le.{0} Rat Rat.instLERat (OfNat.ofNat.{0} Rat 0 (Rat.instOfNatRat 0)) (padicNorm p q) +Case conversion may be inaccurate. Consider using '#align padic_norm.nonneg padicNorm.nonnegₓ'. -/ /-- The `p`-adic norm is nonnegative. -/ protected theorem nonneg (q : ℚ) : 0 ≤ padicNorm p q := if hq : q = 0 then by simp [hq, padicNorm] @@ -70,16 +84,26 @@ protected theorem nonneg (q : ℚ) : 0 ≤ padicNorm p q := exact_mod_cast Nat.zero_le _ #align padic_norm.nonneg padicNorm.nonneg +#print padicNorm.zero /- /-- The `p`-adic norm of `0` is `0`. -/ @[simp] protected theorem zero : padicNorm p 0 = 0 := by simp [padicNorm] #align padic_norm.zero padicNorm.zero +-/ +#print padicNorm.one /- /-- The `p`-adic norm of `1` is `1`. -/ @[simp] protected theorem one : padicNorm p 1 = 1 := by simp [padicNorm] #align padic_norm.one padicNorm.one +-/ +/- warning: padic_norm.padic_norm_p -> padicNorm.padicNorm_p is a dubious translation: +lean 3 declaration is + forall {p : Nat}, (LT.lt.{0} Nat Nat.hasLt (OfNat.ofNat.{0} Nat 1 (OfNat.mk.{0} Nat 1 (One.one.{0} Nat Nat.hasOne))) p) -> (Eq.{1} Rat (padicNorm p ((fun (a : Type) (b : Type) [self : HasLiftT.{1, 1} a b] => self.0) Nat Rat (HasLiftT.mk.{1, 1} Nat Rat (CoeTCₓ.coe.{1, 1} Nat Rat (Nat.castCoe.{0} Rat (AddMonoidWithOne.toNatCast.{0} Rat (AddGroupWithOne.toAddMonoidWithOne.{0} Rat (NonAssocRing.toAddGroupWithOne.{0} Rat (Ring.toNonAssocRing.{0} Rat (StrictOrderedRing.toRing.{0} Rat (LinearOrderedRing.toStrictOrderedRing.{0} Rat Rat.linearOrderedRing))))))))) p)) (Inv.inv.{0} Rat Rat.hasInv ((fun (a : Type) (b : Type) [self : HasLiftT.{1, 1} a b] => self.0) Nat Rat (HasLiftT.mk.{1, 1} Nat Rat (CoeTCₓ.coe.{1, 1} Nat Rat (Nat.castCoe.{0} Rat (AddMonoidWithOne.toNatCast.{0} Rat (AddGroupWithOne.toAddMonoidWithOne.{0} Rat (NonAssocRing.toAddGroupWithOne.{0} Rat (Ring.toNonAssocRing.{0} Rat (StrictOrderedRing.toRing.{0} Rat (LinearOrderedRing.toStrictOrderedRing.{0} Rat Rat.linearOrderedRing))))))))) p))) +but is expected to have type + forall {p : Nat}, (LT.lt.{0} Nat instLTNat (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)) p) -> (Eq.{1} Rat (padicNorm p (Nat.cast.{0} Rat (NonAssocRing.toNatCast.{0} Rat (Ring.toNonAssocRing.{0} Rat (DivisionRing.toRing.{0} Rat Rat.divisionRing))) p)) (Inv.inv.{0} Rat Rat.instInvRat (Nat.cast.{0} Rat (NonAssocRing.toNatCast.{0} Rat (Ring.toNonAssocRing.{0} Rat (DivisionRing.toRing.{0} Rat Rat.divisionRing))) p))) +Case conversion may be inaccurate. Consider using '#align padic_norm.padic_norm_p padicNorm.padicNorm_pₓ'. -/ /-- The `p`-adic norm of `p` is `p⁻¹` if `p > 1`. See also `padic_norm.padic_norm_p_of_prime` for a version assuming `p` is prime. -/ @@ -87,6 +111,12 @@ theorem padicNorm_p (hp : 1 < p) : padicNorm p p = p⁻¹ := by simp [padicNorm, (pos_of_gt hp).ne', padicValNat.self hp] #align padic_norm.padic_norm_p padicNorm.padicNorm_p +/- warning: padic_norm.padic_norm_p_of_prime -> padicNorm.padicNorm_p_of_prime is a dubious translation: +lean 3 declaration is + forall {p : Nat} [_inst_1 : Fact (Nat.Prime p)], Eq.{1} Rat (padicNorm p ((fun (a : Type) (b : Type) [self : HasLiftT.{1, 1} a b] => self.0) Nat Rat (HasLiftT.mk.{1, 1} Nat Rat (CoeTCₓ.coe.{1, 1} Nat Rat (Nat.castCoe.{0} Rat (AddMonoidWithOne.toNatCast.{0} Rat (AddGroupWithOne.toAddMonoidWithOne.{0} Rat (NonAssocRing.toAddGroupWithOne.{0} Rat (Ring.toNonAssocRing.{0} Rat (StrictOrderedRing.toRing.{0} Rat (LinearOrderedRing.toStrictOrderedRing.{0} Rat Rat.linearOrderedRing))))))))) p)) (Inv.inv.{0} Rat Rat.hasInv ((fun (a : Type) (b : Type) [self : HasLiftT.{1, 1} a b] => self.0) Nat Rat (HasLiftT.mk.{1, 1} Nat Rat (CoeTCₓ.coe.{1, 1} Nat Rat (Nat.castCoe.{0} Rat (AddMonoidWithOne.toNatCast.{0} Rat (AddGroupWithOne.toAddMonoidWithOne.{0} Rat (NonAssocRing.toAddGroupWithOne.{0} Rat (Ring.toNonAssocRing.{0} Rat (StrictOrderedRing.toRing.{0} Rat (LinearOrderedRing.toStrictOrderedRing.{0} Rat Rat.linearOrderedRing))))))))) p)) +but is expected to have type + forall {p : Nat} [_inst_1 : Fact (Nat.Prime p)], Eq.{1} Rat (padicNorm p (Nat.cast.{0} Rat (NonAssocRing.toNatCast.{0} Rat (Ring.toNonAssocRing.{0} Rat (DivisionRing.toRing.{0} Rat Rat.divisionRing))) p)) (Inv.inv.{0} Rat Rat.instInvRat (Nat.cast.{0} Rat (NonAssocRing.toNatCast.{0} Rat (Ring.toNonAssocRing.{0} Rat (DivisionRing.toRing.{0} Rat Rat.divisionRing))) p)) +Case conversion may be inaccurate. Consider using '#align padic_norm.padic_norm_p_of_prime padicNorm.padicNorm_p_of_primeₓ'. -/ /-- The `p`-adic norm of `p` is `p⁻¹` if `p` is prime. See also `padic_norm.padic_norm_p` for a version assuming `1 < p`. -/ @@ -95,6 +125,12 @@ theorem padicNorm_p_of_prime [Fact p.Prime] : padicNorm p p = p⁻¹ := padicNorm_p <| Nat.Prime.one_lt (Fact.out _) #align padic_norm.padic_norm_p_of_prime padicNorm.padicNorm_p_of_prime +/- warning: padic_norm.padic_norm_of_prime_of_ne -> padicNorm.padicNorm_of_prime_of_ne is a dubious translation: +lean 3 declaration is + forall {p : Nat} {q : Nat} [p_prime : Fact (Nat.Prime p)] [q_prime : Fact (Nat.Prime q)], (Ne.{1} Nat p q) -> (Eq.{1} Rat (padicNorm p ((fun (a : Type) (b : Type) [self : HasLiftT.{1, 1} a b] => self.0) Nat Rat (HasLiftT.mk.{1, 1} Nat Rat (CoeTCₓ.coe.{1, 1} Nat Rat (Nat.castCoe.{0} Rat (AddMonoidWithOne.toNatCast.{0} Rat (AddGroupWithOne.toAddMonoidWithOne.{0} Rat (NonAssocRing.toAddGroupWithOne.{0} Rat (Ring.toNonAssocRing.{0} Rat (StrictOrderedRing.toRing.{0} Rat (LinearOrderedRing.toStrictOrderedRing.{0} Rat Rat.linearOrderedRing))))))))) q)) (OfNat.ofNat.{0} Rat 1 (OfNat.mk.{0} Rat 1 (One.one.{0} Rat Rat.hasOne)))) +but is expected to have type + forall {p : Nat} {q : Nat} [p_prime : Fact (Nat.Prime p)] [q_prime : Fact (Nat.Prime q)], (Ne.{1} Nat p q) -> (Eq.{1} Rat (padicNorm p (Nat.cast.{0} Rat (NonAssocRing.toNatCast.{0} Rat (Ring.toNonAssocRing.{0} Rat (DivisionRing.toRing.{0} Rat Rat.divisionRing))) q)) (OfNat.ofNat.{0} Rat 1 (Rat.instOfNatRat 1))) +Case conversion may be inaccurate. Consider using '#align padic_norm.padic_norm_of_prime_of_ne padicNorm.padicNorm_of_prime_of_neₓ'. -/ /-- The `p`-adic norm of `q` is `1` if `q` is prime and not equal to `p`. -/ theorem padicNorm_of_prime_of_ne {q : ℕ} [p_prime : Fact p.Prime] [q_prime : Fact q.Prime] (neq : p ≠ q) : padicNorm p q = 1 := @@ -103,6 +139,12 @@ theorem padicNorm_of_prime_of_ne {q : ℕ} [p_prime : Fact p.Prime] [q_prime : F simp [padicNorm, p, q_prime.1.1, q_prime.1.NeZero] #align padic_norm.padic_norm_of_prime_of_ne padicNorm.padicNorm_of_prime_of_ne +/- warning: padic_norm.padic_norm_p_lt_one -> padicNorm.padicNorm_p_lt_one is a dubious translation: +lean 3 declaration is + forall {p : Nat}, (LT.lt.{0} Nat Nat.hasLt (OfNat.ofNat.{0} Nat 1 (OfNat.mk.{0} Nat 1 (One.one.{0} Nat Nat.hasOne))) p) -> (LT.lt.{0} Rat Rat.hasLt (padicNorm p ((fun (a : Type) (b : Type) [self : HasLiftT.{1, 1} a b] => self.0) Nat Rat (HasLiftT.mk.{1, 1} Nat Rat (CoeTCₓ.coe.{1, 1} Nat Rat (Nat.castCoe.{0} Rat (AddMonoidWithOne.toNatCast.{0} Rat (AddGroupWithOne.toAddMonoidWithOne.{0} Rat (NonAssocRing.toAddGroupWithOne.{0} Rat (Ring.toNonAssocRing.{0} Rat (StrictOrderedRing.toRing.{0} Rat (LinearOrderedRing.toStrictOrderedRing.{0} Rat Rat.linearOrderedRing))))))))) p)) (OfNat.ofNat.{0} Rat 1 (OfNat.mk.{0} Rat 1 (One.one.{0} Rat Rat.hasOne)))) +but is expected to have type + forall {p : Nat}, (LT.lt.{0} Nat instLTNat (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)) p) -> (LT.lt.{0} Rat Rat.instLTRat_1 (padicNorm p (Nat.cast.{0} Rat (NonAssocRing.toNatCast.{0} Rat (Ring.toNonAssocRing.{0} Rat (DivisionRing.toRing.{0} Rat Rat.divisionRing))) p)) (OfNat.ofNat.{0} Rat 1 (Rat.instOfNatRat 1))) +Case conversion may be inaccurate. Consider using '#align padic_norm.padic_norm_p_lt_one padicNorm.padicNorm_p_lt_oneₓ'. -/ /-- The `p`-adic norm of `p` is less than `1` if `1 < p`. See also `padic_norm.padic_norm_p_lt_one_of_prime` for a version assuming `p` is prime. -/ @@ -112,6 +154,12 @@ theorem padicNorm_p_lt_one (hp : 1 < p) : padicNorm p p < 1 := exact_mod_cast Or.inr hp #align padic_norm.padic_norm_p_lt_one padicNorm.padicNorm_p_lt_one +/- warning: padic_norm.padic_norm_p_lt_one_of_prime -> padicNorm.padicNorm_p_lt_one_of_prime is a dubious translation: +lean 3 declaration is + forall {p : Nat} [_inst_1 : Fact (Nat.Prime p)], LT.lt.{0} Rat Rat.hasLt (padicNorm p ((fun (a : Type) (b : Type) [self : HasLiftT.{1, 1} a b] => self.0) Nat Rat (HasLiftT.mk.{1, 1} Nat Rat (CoeTCₓ.coe.{1, 1} Nat Rat (Nat.castCoe.{0} Rat (AddMonoidWithOne.toNatCast.{0} Rat (AddGroupWithOne.toAddMonoidWithOne.{0} Rat (NonAssocRing.toAddGroupWithOne.{0} Rat (Ring.toNonAssocRing.{0} Rat (StrictOrderedRing.toRing.{0} Rat (LinearOrderedRing.toStrictOrderedRing.{0} Rat Rat.linearOrderedRing))))))))) p)) (OfNat.ofNat.{0} Rat 1 (OfNat.mk.{0} Rat 1 (One.one.{0} Rat Rat.hasOne))) +but is expected to have type + forall {p : Nat} [_inst_1 : Fact (Nat.Prime p)], LT.lt.{0} Rat Rat.instLTRat_1 (padicNorm p (Nat.cast.{0} Rat (NonAssocRing.toNatCast.{0} Rat (Ring.toNonAssocRing.{0} Rat (DivisionRing.toRing.{0} Rat Rat.divisionRing))) p)) (OfNat.ofNat.{0} Rat 1 (Rat.instOfNatRat 1)) +Case conversion may be inaccurate. Consider using '#align padic_norm.padic_norm_p_lt_one_of_prime padicNorm.padicNorm_p_lt_one_of_primeₓ'. -/ /-- The `p`-adic norm of `p` is less than `1` if `p` is prime. See also `padic_norm.padic_norm_p_lt_one` for a version assuming `1 < p`. -/ @@ -119,21 +167,30 @@ theorem padicNorm_p_lt_one_of_prime [Fact p.Prime] : padicNorm p p < 1 := padicNorm_p_lt_one <| Nat.Prime.one_lt (Fact.out _) #align padic_norm.padic_norm_p_lt_one_of_prime padicNorm.padicNorm_p_lt_one_of_prime +/- warning: padic_norm.values_discrete -> padicNorm.values_discrete is a dubious translation: +lean 3 declaration is + forall {p : Nat} {q : Rat}, (Ne.{1} Rat q (OfNat.ofNat.{0} Rat 0 (OfNat.mk.{0} Rat 0 (Zero.zero.{0} Rat Rat.hasZero)))) -> (Exists.{1} Int (fun (z : Int) => Eq.{1} Rat (padicNorm p q) (HPow.hPow.{0, 0, 0} Rat Int Rat (instHPow.{0, 0} Rat Int (DivInvMonoid.Pow.{0} Rat (DivisionRing.toDivInvMonoid.{0} Rat Rat.divisionRing))) ((fun (a : Type) (b : Type) [self : HasLiftT.{1, 1} a b] => self.0) Nat Rat (HasLiftT.mk.{1, 1} Nat Rat (CoeTCₓ.coe.{1, 1} Nat Rat (Nat.castCoe.{0} Rat (AddMonoidWithOne.toNatCast.{0} Rat (AddGroupWithOne.toAddMonoidWithOne.{0} Rat (NonAssocRing.toAddGroupWithOne.{0} Rat (Ring.toNonAssocRing.{0} Rat (StrictOrderedRing.toRing.{0} Rat (LinearOrderedRing.toStrictOrderedRing.{0} Rat Rat.linearOrderedRing))))))))) p) (Neg.neg.{0} Int Int.hasNeg z)))) +but is expected to have type + forall {p : Nat} {q : Rat}, (Ne.{1} Rat q (OfNat.ofNat.{0} Rat 0 (Rat.instOfNatRat 0))) -> (Exists.{1} Int (fun (z : Int) => Eq.{1} Rat (padicNorm p q) (HPow.hPow.{0, 0, 0} Rat Int Rat (instHPow.{0, 0} Rat Int (DivInvMonoid.Pow.{0} Rat (DivisionRing.toDivInvMonoid.{0} Rat Rat.divisionRing))) (Nat.cast.{0} Rat (NonAssocRing.toNatCast.{0} Rat (Ring.toNonAssocRing.{0} Rat (DivisionRing.toRing.{0} Rat Rat.divisionRing))) p) (Neg.neg.{0} Int Int.instNegInt z)))) +Case conversion may be inaccurate. Consider using '#align padic_norm.values_discrete padicNorm.values_discreteₓ'. -/ /-- `padic_norm p q` takes discrete values `p ^ -z` for `z : ℤ`. -/ protected theorem values_discrete {q : ℚ} (hq : q ≠ 0) : ∃ z : ℤ, padicNorm p q = p ^ (-z) := ⟨padicValRat p q, by simp [padicNorm, hq]⟩ #align padic_norm.values_discrete padicNorm.values_discrete +#print padicNorm.neg /- /-- `padic_norm p` is symmetric. -/ @[simp] protected theorem neg (q : ℚ) : padicNorm p (-q) = padicNorm p q := if hq : q = 0 then by simp [hq] else by simp [padicNorm, hq] #align padic_norm.neg padicNorm.neg +-/ variable [hp : Fact p.Prime] include hp +#print padicNorm.nonzero /- /-- If `q ≠ 0`, then `padic_norm p q ≠ 0`. -/ protected theorem nonzero {q : ℚ} (hq : q ≠ 0) : padicNorm p q ≠ 0 := by @@ -141,7 +198,9 @@ protected theorem nonzero {q : ℚ} (hq : q ≠ 0) : padicNorm p q ≠ 0 := apply zpow_ne_zero_of_ne_zero exact_mod_cast ne_of_gt hp.1.Pos #align padic_norm.nonzero padicNorm.nonzero +-/ +#print padicNorm.zero_of_padicNorm_eq_zero /- /-- If the `p`-adic norm of `q` is 0, then `q` is `0`. -/ theorem zero_of_padicNorm_eq_zero {q : ℚ} (h : padicNorm p q = 0) : q = 0 := by @@ -151,7 +210,9 @@ theorem zero_of_padicNorm_eq_zero {q : ℚ} (h : padicNorm p q = 0) : q = 0 := apply zpow_ne_zero_of_ne_zero exact_mod_cast hp.1.NeZero #align padic_norm.zero_of_padic_norm_eq_zero padicNorm.zero_of_padicNorm_eq_zero +-/ +#print padicNorm.mul /- /-- The `p`-adic norm is multiplicative. -/ @[simp] protected theorem mul (q r : ℚ) : padicNorm p (q * r) = padicNorm p q * padicNorm p r := @@ -163,14 +224,23 @@ protected theorem mul (q r : ℚ) : padicNorm p (q * r) = padicNorm p q * padicN have : (p : ℚ) ≠ 0 := by simp [hp.1.NeZero] simp [padicNorm, *, padicValRat.mul, zpow_add₀ this, mul_comm] #align padic_norm.mul padicNorm.mul +-/ +#print padicNorm.div /- /-- The `p`-adic norm respects division. -/ @[simp] protected theorem div (q r : ℚ) : padicNorm p (q / r) = padicNorm p q / padicNorm p r := if hr : r = 0 then by simp [hr] else eq_div_of_mul_eq (padicNorm.nonzero hr) (by rw [← padicNorm.mul, div_mul_cancel _ hr]) #align padic_norm.div padicNorm.div +-/ +/- warning: padic_norm.of_int -> padicNorm.of_int is a dubious translation: +lean 3 declaration is + forall {p : Nat} [hp : Fact (Nat.Prime p)] (z : Int), LE.le.{0} Rat Rat.hasLe (padicNorm p ((fun (a : Type) (b : Type) [self : HasLiftT.{1, 1} a b] => self.0) Int Rat (HasLiftT.mk.{1, 1} Int Rat (CoeTCₓ.coe.{1, 1} Int Rat (Int.castCoe.{0} Rat Rat.hasIntCast))) z)) (OfNat.ofNat.{0} Rat 1 (OfNat.mk.{0} Rat 1 (One.one.{0} Rat Rat.hasOne))) +but is expected to have type + forall {p : Nat} [hp : Fact (Nat.Prime p)] (z : Int), LE.le.{0} Rat Rat.instLERat (padicNorm p (Int.cast.{0} Rat Rat.instIntCastRat z)) (OfNat.ofNat.{0} Rat 1 (Rat.instOfNatRat 1)) +Case conversion may be inaccurate. Consider using '#align padic_norm.of_int padicNorm.of_intₓ'. -/ /-- The `p`-adic norm of an integer is at most `1`. -/ protected theorem of_int (z : ℤ) : padicNorm p z ≤ 1 := if hz : z = 0 then by simp [hz, zero_le_one] @@ -206,6 +276,12 @@ private theorem nonarchimedean_aux {q r : ℚ} (h : padicValRat p q ≤ padicVal apply min_le_padic_val_rat_add <;> assumption #align padic_norm.nonarchimedean_aux padic_norm.nonarchimedean_aux +/- warning: padic_norm.nonarchimedean -> padicNorm.nonarchimedean is a dubious translation: +lean 3 declaration is + forall {p : Nat} [hp : Fact (Nat.Prime p)] {q : Rat} {r : Rat}, LE.le.{0} Rat Rat.hasLe (padicNorm p (HAdd.hAdd.{0, 0, 0} Rat Rat Rat (instHAdd.{0} Rat Rat.hasAdd) q r)) (LinearOrder.max.{0} Rat Rat.linearOrder (padicNorm p q) (padicNorm p r)) +but is expected to have type + forall {p : Nat} [hp : Fact (Nat.Prime p)] {q : Rat} {r : Rat}, LE.le.{0} Rat Rat.instLERat (padicNorm p (HAdd.hAdd.{0, 0, 0} Rat Rat Rat (instHAdd.{0} Rat Rat.instAddRat) q r)) (Max.max.{0} Rat (LinearOrderedRing.toMax.{0} Rat Rat.instLinearOrderedRingRat) (padicNorm p q) (padicNorm p r)) +Case conversion may be inaccurate. Consider using '#align padic_norm.nonarchimedean padicNorm.nonarchimedeanₓ'. -/ /-- The `p`-adic norm is nonarchimedean: the norm of `p + q` is at most the max of the norm of `p` and the norm of `q`. -/ protected theorem nonarchimedean {q r : ℚ} : @@ -217,6 +293,12 @@ protected theorem nonarchimedean {q r : ℚ} : exact nonarchimedean_aux hle #align padic_norm.nonarchimedean padicNorm.nonarchimedean +/- warning: padic_norm.triangle_ineq -> padicNorm.triangle_ineq is a dubious translation: +lean 3 declaration is + forall {p : Nat} [hp : Fact (Nat.Prime p)] (q : Rat) (r : Rat), LE.le.{0} Rat Rat.hasLe (padicNorm p (HAdd.hAdd.{0, 0, 0} Rat Rat Rat (instHAdd.{0} Rat Rat.hasAdd) q r)) (HAdd.hAdd.{0, 0, 0} Rat Rat Rat (instHAdd.{0} Rat Rat.hasAdd) (padicNorm p q) (padicNorm p r)) +but is expected to have type + forall {p : Nat} [hp : Fact (Nat.Prime p)] (q : Rat) (r : Rat), LE.le.{0} Rat Rat.instLERat (padicNorm p (HAdd.hAdd.{0, 0, 0} Rat Rat Rat (instHAdd.{0} Rat Rat.instAddRat) q r)) (HAdd.hAdd.{0, 0, 0} Rat Rat Rat (instHAdd.{0} Rat Rat.instAddRat) (padicNorm p q) (padicNorm p r)) +Case conversion may be inaccurate. Consider using '#align padic_norm.triangle_ineq padicNorm.triangle_ineqₓ'. -/ /-- The `p`-adic norm respects the triangle inequality: the norm of `p + q` is at most the norm of `p` plus the norm of `q`. -/ theorem triangle_ineq (q r : ℚ) : padicNorm p (q + r) ≤ padicNorm p q + padicNorm p r := @@ -227,12 +309,24 @@ theorem triangle_ineq (q r : ℚ) : padicNorm p (q + r) ≤ padicNorm p q + padi #align padic_norm.triangle_ineq padicNorm.triangle_ineq +/- warning: padic_norm.sub -> padicNorm.sub is a dubious translation: +lean 3 declaration is + forall {p : Nat} [hp : Fact (Nat.Prime p)] {q : Rat} {r : Rat}, LE.le.{0} Rat Rat.hasLe (padicNorm p (HSub.hSub.{0, 0, 0} Rat Rat Rat (instHSub.{0} Rat (SubNegMonoid.toHasSub.{0} Rat (AddGroup.toSubNegMonoid.{0} Rat Rat.addGroup))) q r)) (LinearOrder.max.{0} Rat Rat.linearOrder (padicNorm p q) (padicNorm p r)) +but is expected to have type + forall {p : Nat} [hp : Fact (Nat.Prime p)] {q : Rat} {r : Rat}, LE.le.{0} Rat Rat.instLERat (padicNorm p (HSub.hSub.{0, 0, 0} Rat Rat Rat (instHSub.{0} Rat Rat.instSubRat) q r)) (Max.max.{0} Rat (LinearOrderedRing.toMax.{0} Rat Rat.instLinearOrderedRingRat) (padicNorm p q) (padicNorm p r)) +Case conversion may be inaccurate. Consider using '#align padic_norm.sub padicNorm.subₓ'. -/ /-- The `p`-adic norm of a difference is at most the max of each component. Restates the archimedean property of the `p`-adic norm. -/ protected theorem sub {q r : ℚ} : padicNorm p (q - r) ≤ max (padicNorm p q) (padicNorm p r) := by rw [sub_eq_add_neg, ← padicNorm.neg r] <;> apply padicNorm.nonarchimedean #align padic_norm.sub padicNorm.sub +/- warning: padic_norm.add_eq_max_of_ne -> padicNorm.add_eq_max_of_ne is a dubious translation: +lean 3 declaration is + forall {p : Nat} [hp : Fact (Nat.Prime p)] {q : Rat} {r : Rat}, (Ne.{1} Rat (padicNorm p q) (padicNorm p r)) -> (Eq.{1} Rat (padicNorm p (HAdd.hAdd.{0, 0, 0} Rat Rat Rat (instHAdd.{0} Rat Rat.hasAdd) q r)) (LinearOrder.max.{0} Rat Rat.linearOrder (padicNorm p q) (padicNorm p r))) +but is expected to have type + forall {p : Nat} [hp : Fact (Nat.Prime p)] {q : Rat} {r : Rat}, (Ne.{1} Rat (padicNorm p q) (padicNorm p r)) -> (Eq.{1} Rat (padicNorm p (HAdd.hAdd.{0, 0, 0} Rat Rat Rat (instHAdd.{0} Rat Rat.instAddRat) q r)) (Max.max.{0} Rat (LinearOrderedRing.toMax.{0} Rat Rat.instLinearOrderedRingRat) (padicNorm p q) (padicNorm p r))) +Case conversion may be inaccurate. Consider using '#align padic_norm.add_eq_max_of_ne padicNorm.add_eq_max_of_neₓ'. -/ /-- If the `p`-adic norms of `q` and `r` are different, then the norm of `q + r` is equal to the max of the norms of `q` and `r`. -/ theorem add_eq_max_of_ne {q r : ℚ} (hne : padicNorm p q ≠ padicNorm p r) : @@ -269,6 +363,12 @@ instance : IsAbsoluteValue (padicNorm p) abv_add := padicNorm.triangle_ineq abv_mul := padicNorm.mul +/- warning: padic_norm.dvd_iff_norm_le -> padicNorm.dvd_iff_norm_le is a dubious translation: +lean 3 declaration is + forall {p : Nat} [hp : Fact (Nat.Prime p)] {n : Nat} {z : Int}, Iff (Dvd.Dvd.{0} Int (semigroupDvd.{0} Int Int.semigroup) ((fun (a : Type) (b : Type) [self : HasLiftT.{1, 1} a b] => self.0) Nat Int (HasLiftT.mk.{1, 1} Nat Int (CoeTCₓ.coe.{1, 1} Nat Int (coeBase.{1, 1} Nat Int Int.hasCoe))) (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat (Monoid.Pow.{0} Nat Nat.monoid)) p n)) z) (LE.le.{0} Rat Rat.hasLe (padicNorm p ((fun (a : Type) (b : Type) [self : HasLiftT.{1, 1} a b] => self.0) Int Rat (HasLiftT.mk.{1, 1} Int Rat (CoeTCₓ.coe.{1, 1} Int Rat (Int.castCoe.{0} Rat Rat.hasIntCast))) z)) (HPow.hPow.{0, 0, 0} Rat Int Rat (instHPow.{0, 0} Rat Int (DivInvMonoid.Pow.{0} Rat (DivisionRing.toDivInvMonoid.{0} Rat Rat.divisionRing))) ((fun (a : Type) (b : Type) [self : HasLiftT.{1, 1} a b] => self.0) Nat Rat (HasLiftT.mk.{1, 1} Nat Rat (CoeTCₓ.coe.{1, 1} Nat Rat (Nat.castCoe.{0} Rat (AddMonoidWithOne.toNatCast.{0} Rat (AddGroupWithOne.toAddMonoidWithOne.{0} Rat (NonAssocRing.toAddGroupWithOne.{0} Rat (Ring.toNonAssocRing.{0} Rat (StrictOrderedRing.toRing.{0} Rat (LinearOrderedRing.toStrictOrderedRing.{0} Rat Rat.linearOrderedRing))))))))) p) (Neg.neg.{0} Int Int.hasNeg ((fun (a : Type) (b : Type) [self : HasLiftT.{1, 1} a b] => self.0) Nat Int (HasLiftT.mk.{1, 1} Nat Int (CoeTCₓ.coe.{1, 1} Nat Int (coeBase.{1, 1} Nat Int Int.hasCoe))) n)))) +but is expected to have type + forall {p : Nat} [hp : Fact (Nat.Prime p)] {n : Nat} {z : Int}, Iff (Dvd.dvd.{0} Int Int.instDvdInt (Nat.cast.{0} Int instNatCastInt (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat instPowNat) p n)) z) (LE.le.{0} Rat Rat.instLERat (padicNorm p (Int.cast.{0} Rat Rat.instIntCastRat z)) (HPow.hPow.{0, 0, 0} Rat Int Rat (instHPow.{0, 0} Rat Int (DivInvMonoid.Pow.{0} Rat (DivisionRing.toDivInvMonoid.{0} Rat Rat.divisionRing))) (Nat.cast.{0} Rat (NonAssocRing.toNatCast.{0} Rat (Ring.toNonAssocRing.{0} Rat (DivisionRing.toRing.{0} Rat Rat.divisionRing))) p) (Neg.neg.{0} Int Int.instNegInt (Nat.cast.{0} Int instNatCastInt n)))) +Case conversion may be inaccurate. Consider using '#align padic_norm.dvd_iff_norm_le padicNorm.dvd_iff_norm_leₓ'. -/ theorem dvd_iff_norm_le {n : ℕ} {z : ℤ} : ↑(p ^ n) ∣ z ↔ padicNorm p z ≤ p ^ (-n : ℤ) := by unfold padicNorm; split_ifs with hz @@ -286,6 +386,12 @@ theorem dvd_iff_norm_le {n : ℕ} {z : ℤ} : ↑(p ^ n) ∣ z ↔ padicNorm p z · exact_mod_cast hp.1.one_lt #align padic_norm.dvd_iff_norm_le padicNorm.dvd_iff_norm_le +/- warning: padic_norm.int_eq_one_iff -> padicNorm.int_eq_one_iff is a dubious translation: +lean 3 declaration is + forall {p : Nat} [hp : Fact (Nat.Prime p)] (m : Int), Iff (Eq.{1} Rat (padicNorm p ((fun (a : Type) (b : Type) [self : HasLiftT.{1, 1} a b] => self.0) Int Rat (HasLiftT.mk.{1, 1} Int Rat (CoeTCₓ.coe.{1, 1} Int Rat (Int.castCoe.{0} Rat Rat.hasIntCast))) m)) (OfNat.ofNat.{0} Rat 1 (OfNat.mk.{0} Rat 1 (One.one.{0} Rat Rat.hasOne)))) (Not (Dvd.Dvd.{0} Int (semigroupDvd.{0} Int Int.semigroup) ((fun (a : Type) (b : Type) [self : HasLiftT.{1, 1} a b] => self.0) Nat Int (HasLiftT.mk.{1, 1} Nat Int (CoeTCₓ.coe.{1, 1} Nat Int (coeBase.{1, 1} Nat Int Int.hasCoe))) p) m)) +but is expected to have type + forall {p : Nat} [hp : Fact (Nat.Prime p)] (m : Int), Iff (Eq.{1} Rat (padicNorm p (Int.cast.{0} Rat Rat.instIntCastRat m)) (OfNat.ofNat.{0} Rat 1 (Rat.instOfNatRat 1))) (Not (Dvd.dvd.{0} Int Int.instDvdInt (Nat.cast.{0} Int instNatCastInt p) m)) +Case conversion may be inaccurate. Consider using '#align padic_norm.int_eq_one_iff padicNorm.int_eq_one_iffₓ'. -/ /-- The `p`-adic norm of an integer `m` is one iff `p` doesn't divide `m`. -/ theorem int_eq_one_iff (m : ℤ) : padicNorm p m = 1 ↔ ¬(p : ℤ) ∣ m := by @@ -309,27 +415,52 @@ theorem int_eq_one_iff (m : ℤ) : padicNorm p m = 1 ↔ ¬(p : ℤ) ∣ m := rw [← zpow_zero (p : ℚ), zpow_inj] <;> linarith #align padic_norm.int_eq_one_iff padicNorm.int_eq_one_iff +/- warning: padic_norm.int_lt_one_iff -> padicNorm.int_lt_one_iff is a dubious translation: +lean 3 declaration is + forall {p : Nat} [hp : Fact (Nat.Prime p)] (m : Int), Iff (LT.lt.{0} Rat Rat.hasLt (padicNorm p ((fun (a : Type) (b : Type) [self : HasLiftT.{1, 1} a b] => self.0) Int Rat (HasLiftT.mk.{1, 1} Int Rat (CoeTCₓ.coe.{1, 1} Int Rat (Int.castCoe.{0} Rat Rat.hasIntCast))) m)) (OfNat.ofNat.{0} Rat 1 (OfNat.mk.{0} Rat 1 (One.one.{0} Rat Rat.hasOne)))) (Dvd.Dvd.{0} Int (semigroupDvd.{0} Int Int.semigroup) ((fun (a : Type) (b : Type) [self : HasLiftT.{1, 1} a b] => self.0) Nat Int (HasLiftT.mk.{1, 1} Nat Int (CoeTCₓ.coe.{1, 1} Nat Int (coeBase.{1, 1} Nat Int Int.hasCoe))) p) m) +but is expected to have type + forall {p : Nat} [hp : Fact (Nat.Prime p)] (m : Int), Iff (LT.lt.{0} Rat Rat.instLTRat_1 (padicNorm p (Int.cast.{0} Rat Rat.instIntCastRat m)) (OfNat.ofNat.{0} Rat 1 (Rat.instOfNatRat 1))) (Dvd.dvd.{0} Int Int.instDvdInt (Nat.cast.{0} Int instNatCastInt p) m) +Case conversion may be inaccurate. Consider using '#align padic_norm.int_lt_one_iff padicNorm.int_lt_one_iffₓ'. -/ theorem int_lt_one_iff (m : ℤ) : padicNorm p m < 1 ↔ (p : ℤ) ∣ m := by rw [← not_iff_not, ← int_eq_one_iff, eq_iff_le_not_lt] simp only [padicNorm.of_int, true_and_iff] #align padic_norm.int_lt_one_iff padicNorm.int_lt_one_iff +/- warning: padic_norm.of_nat -> padicNorm.of_nat is a dubious translation: +lean 3 declaration is + forall {p : Nat} [hp : Fact (Nat.Prime p)] (m : Nat), LE.le.{0} Rat Rat.hasLe (padicNorm p ((fun (a : Type) (b : Type) [self : HasLiftT.{1, 1} a b] => self.0) Nat Rat (HasLiftT.mk.{1, 1} Nat Rat (CoeTCₓ.coe.{1, 1} Nat Rat (Nat.castCoe.{0} Rat (AddMonoidWithOne.toNatCast.{0} Rat (AddGroupWithOne.toAddMonoidWithOne.{0} Rat (NonAssocRing.toAddGroupWithOne.{0} Rat (Ring.toNonAssocRing.{0} Rat (StrictOrderedRing.toRing.{0} Rat (LinearOrderedRing.toStrictOrderedRing.{0} Rat Rat.linearOrderedRing))))))))) m)) (OfNat.ofNat.{0} Rat 1 (OfNat.mk.{0} Rat 1 (One.one.{0} Rat Rat.hasOne))) +but is expected to have type + forall {p : Nat} [hp : Fact (Nat.Prime p)] (m : Nat), LE.le.{0} Rat Rat.instLERat (padicNorm p (Nat.cast.{0} Rat (NonAssocRing.toNatCast.{0} Rat (Ring.toNonAssocRing.{0} Rat (DivisionRing.toRing.{0} Rat Rat.divisionRing))) m)) (OfNat.ofNat.{0} Rat 1 (Rat.instOfNatRat 1)) +Case conversion may be inaccurate. Consider using '#align padic_norm.of_nat padicNorm.of_natₓ'. -/ theorem of_nat (m : ℕ) : padicNorm p m ≤ 1 := padicNorm.of_int (m : ℤ) #align padic_norm.of_nat padicNorm.of_nat +/- warning: padic_norm.nat_eq_one_iff -> padicNorm.nat_eq_one_iff is a dubious translation: +lean 3 declaration is + forall {p : Nat} [hp : Fact (Nat.Prime p)] (m : Nat), Iff (Eq.{1} Rat (padicNorm p ((fun (a : Type) (b : Type) [self : HasLiftT.{1, 1} a b] => self.0) Nat Rat (HasLiftT.mk.{1, 1} Nat Rat (CoeTCₓ.coe.{1, 1} Nat Rat (Nat.castCoe.{0} Rat (AddMonoidWithOne.toNatCast.{0} Rat (AddGroupWithOne.toAddMonoidWithOne.{0} Rat (NonAssocRing.toAddGroupWithOne.{0} Rat (Ring.toNonAssocRing.{0} Rat (StrictOrderedRing.toRing.{0} Rat (LinearOrderedRing.toStrictOrderedRing.{0} Rat Rat.linearOrderedRing))))))))) m)) (OfNat.ofNat.{0} Rat 1 (OfNat.mk.{0} Rat 1 (One.one.{0} Rat Rat.hasOne)))) (Not (Dvd.Dvd.{0} Nat Nat.hasDvd p m)) +but is expected to have type + forall {p : Nat} [hp : Fact (Nat.Prime p)] (m : Nat), Iff (Eq.{1} Rat (padicNorm p (Nat.cast.{0} Rat (NonAssocRing.toNatCast.{0} Rat (Ring.toNonAssocRing.{0} Rat (DivisionRing.toRing.{0} Rat Rat.divisionRing))) m)) (OfNat.ofNat.{0} Rat 1 (Rat.instOfNatRat 1))) (Not (Dvd.dvd.{0} Nat Nat.instDvdNat p m)) +Case conversion may be inaccurate. Consider using '#align padic_norm.nat_eq_one_iff padicNorm.nat_eq_one_iffₓ'. -/ /-- The `p`-adic norm of a natural `m` is one iff `p` doesn't divide `m`. -/ theorem nat_eq_one_iff (m : ℕ) : padicNorm p m = 1 ↔ ¬p ∣ m := by simp only [← Int.coe_nat_dvd, ← int_eq_one_iff, Int.cast_ofNat] #align padic_norm.nat_eq_one_iff padicNorm.nat_eq_one_iff +/- warning: padic_norm.nat_lt_one_iff -> padicNorm.nat_lt_one_iff is a dubious translation: +lean 3 declaration is + forall {p : Nat} [hp : Fact (Nat.Prime p)] (m : Nat), Iff (LT.lt.{0} Rat Rat.hasLt (padicNorm p ((fun (a : Type) (b : Type) [self : HasLiftT.{1, 1} a b] => self.0) Nat Rat (HasLiftT.mk.{1, 1} Nat Rat (CoeTCₓ.coe.{1, 1} Nat Rat (Nat.castCoe.{0} Rat (AddMonoidWithOne.toNatCast.{0} Rat (AddGroupWithOne.toAddMonoidWithOne.{0} Rat (NonAssocRing.toAddGroupWithOne.{0} Rat (Ring.toNonAssocRing.{0} Rat (StrictOrderedRing.toRing.{0} Rat (LinearOrderedRing.toStrictOrderedRing.{0} Rat Rat.linearOrderedRing))))))))) m)) (OfNat.ofNat.{0} Rat 1 (OfNat.mk.{0} Rat 1 (One.one.{0} Rat Rat.hasOne)))) (Dvd.Dvd.{0} Nat Nat.hasDvd p m) +but is expected to have type + forall {p : Nat} [hp : Fact (Nat.Prime p)] (m : Nat), Iff (LT.lt.{0} Rat Rat.instLTRat_1 (padicNorm p (Nat.cast.{0} Rat (NonAssocRing.toNatCast.{0} Rat (Ring.toNonAssocRing.{0} Rat (DivisionRing.toRing.{0} Rat Rat.divisionRing))) m)) (OfNat.ofNat.{0} Rat 1 (Rat.instOfNatRat 1))) (Dvd.dvd.{0} Nat Nat.instDvdNat p m) +Case conversion may be inaccurate. Consider using '#align padic_norm.nat_lt_one_iff padicNorm.nat_lt_one_iffₓ'. -/ theorem nat_lt_one_iff (m : ℕ) : padicNorm p m < 1 ↔ p ∣ m := by simp only [← Int.coe_nat_dvd, ← int_lt_one_iff, Int.cast_ofNat] #align padic_norm.nat_lt_one_iff padicNorm.nat_lt_one_iff open BigOperators +#print padicNorm.sum_lt /- theorem sum_lt {α : Type _} {F : α → ℚ} {t : ℚ} {s : Finset α} : s.Nonempty → (∀ i ∈ s, padicNorm p (F i) < t) → padicNorm p (∑ i in s, F i) < t := by classical @@ -343,7 +474,14 @@ theorem sum_lt {α : Type _} {F : α → ℚ} {t : ℚ} {s : Finset α} : (IH hs fun b hb => ht b (Finset.mem_insert_of_mem hb))) · simp_all #align padic_norm.sum_lt padicNorm.sum_lt +-/ +/- warning: padic_norm.sum_le -> padicNorm.sum_le is a dubious translation: +lean 3 declaration is + forall {p : Nat} [hp : Fact (Nat.Prime p)] {α : Type.{u1}} {F : α -> Rat} {t : Rat} {s : Finset.{u1} α}, (Finset.Nonempty.{u1} α s) -> (forall (i : α), (Membership.Mem.{u1, u1} α (Finset.{u1} α) (Finset.hasMem.{u1} α) i s) -> (LE.le.{0} Rat Rat.hasLe (padicNorm p (F i)) t)) -> (LE.le.{0} Rat Rat.hasLe (padicNorm p (Finset.sum.{0, u1} Rat α Rat.addCommMonoid s (fun (i : α) => F i))) t) +but is expected to have type + forall {p : Nat} [hp : Fact (Nat.Prime p)] {α : Type.{u1}} {F : α -> Rat} {t : Rat} {s : Finset.{u1} α}, (Finset.Nonempty.{u1} α s) -> (forall (i : α), (Membership.mem.{u1, u1} α (Finset.{u1} α) (Finset.instMembershipFinset.{u1} α) i s) -> (LE.le.{0} Rat Rat.instLERat (padicNorm p (F i)) t)) -> (LE.le.{0} Rat Rat.instLERat (padicNorm p (Finset.sum.{0, u1} Rat α Rat.addCommMonoid s (fun (i : α) => F i))) t) +Case conversion may be inaccurate. Consider using '#align padic_norm.sum_le padicNorm.sum_leₓ'. -/ theorem sum_le {α : Type _} {F : α → ℚ} {t : ℚ} {s : Finset α} : s.Nonempty → (∀ i ∈ s, padicNorm p (F i) ≤ t) → padicNorm p (∑ i in s, F i) ≤ t := by classical @@ -358,6 +496,7 @@ theorem sum_le {α : Type _} {F : α → ℚ} {t : ℚ} {s : Finset α} : · simp_all #align padic_norm.sum_le padicNorm.sum_le +#print padicNorm.sum_lt' /- theorem sum_lt' {α : Type _} {F : α → ℚ} {t : ℚ} {s : Finset α} (hF : ∀ i ∈ s, padicNorm p (F i) < t) (ht : 0 < t) : padicNorm p (∑ i in s, F i) < t := by @@ -365,7 +504,14 @@ theorem sum_lt' {α : Type _} {F : α → ℚ} {t : ℚ} {s : Finset α} · simp [ht] · exact sum_lt hs hF #align padic_norm.sum_lt' padicNorm.sum_lt' +-/ +/- warning: padic_norm.sum_le' -> padicNorm.sum_le' is a dubious translation: +lean 3 declaration is + forall {p : Nat} [hp : Fact (Nat.Prime p)] {α : Type.{u1}} {F : α -> Rat} {t : Rat} {s : Finset.{u1} α}, (forall (i : α), (Membership.Mem.{u1, u1} α (Finset.{u1} α) (Finset.hasMem.{u1} α) i s) -> (LE.le.{0} Rat Rat.hasLe (padicNorm p (F i)) t)) -> (LE.le.{0} Rat Rat.hasLe (OfNat.ofNat.{0} Rat 0 (OfNat.mk.{0} Rat 0 (Zero.zero.{0} Rat Rat.hasZero))) t) -> (LE.le.{0} Rat Rat.hasLe (padicNorm p (Finset.sum.{0, u1} Rat α Rat.addCommMonoid s (fun (i : α) => F i))) t) +but is expected to have type + forall {p : Nat} [hp : Fact (Nat.Prime p)] {α : Type.{u1}} {F : α -> Rat} {t : Rat} {s : Finset.{u1} α}, (forall (i : α), (Membership.mem.{u1, u1} α (Finset.{u1} α) (Finset.instMembershipFinset.{u1} α) i s) -> (LE.le.{0} Rat Rat.instLERat (padicNorm p (F i)) t)) -> (LE.le.{0} Rat Rat.instLERat (OfNat.ofNat.{0} Rat 0 (Rat.instOfNatRat 0)) t) -> (LE.le.{0} Rat Rat.instLERat (padicNorm p (Finset.sum.{0, u1} Rat α Rat.addCommMonoid s (fun (i : α) => F i))) t) +Case conversion may be inaccurate. Consider using '#align padic_norm.sum_le' padicNorm.sum_le'ₓ'. -/ theorem sum_le' {α : Type _} {F : α → ℚ} {t : ℚ} {s : Finset α} (hF : ∀ i ∈ s, padicNorm p (F i) ≤ t) (ht : 0 ≤ t) : padicNorm p (∑ i in s, F i) ≤ t := by diff --git a/lake-manifest.json b/lake-manifest.json index 0460f2d260..fe83a08c61 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,15 +4,15 @@ [{"git": {"url": "https://github.com/leanprover-community/lean3port.git", "subDir?": null, - "rev": "968bcaebc85e2513af17590b277eaf90b08bf2ab", + "rev": "ccd1ac57ea0c2eef94c3d8752a559d9416e0c5ba", "name": "lean3port", - "inputRev?": "968bcaebc85e2513af17590b277eaf90b08bf2ab"}}, + "inputRev?": "ccd1ac57ea0c2eef94c3d8752a559d9416e0c5ba"}}, {"git": {"url": "https://github.com/leanprover-community/mathlib4.git", "subDir?": null, - "rev": "b531e74af354db6b15768f6db2a983e9b9e32e64", + "rev": "44e938c76645c7acf8b2902aac63c297577cbcbd", "name": "mathlib", - "inputRev?": "b531e74af354db6b15768f6db2a983e9b9e32e64"}}, + "inputRev?": "44e938c76645c7acf8b2902aac63c297577cbcbd"}}, {"git": {"url": "https://github.com/gebner/quote4", "subDir?": null, diff --git a/lakefile.lean b/lakefile.lean index da9138b356..756f44501c 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-03-24-12" +def tag : String := "nightly-2023-03-24-14" 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"@"968bcaebc85e2513af17590b277eaf90b08bf2ab" +require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"ccd1ac57ea0c2eef94c3d8752a559d9416e0c5ba" @[default_target] lean_lib Mathbin where