Skip to content

Commit

Permalink
bump to nightly-2023-05-16-14
Browse files Browse the repository at this point in the history 
mathlib commit leanprover-community/mathlib@0b9eaaa
  • Loading branch information
@leanprover-community-bot
leanprover-community-bot committed May 16, 2023
1 parent 138da42 commit b356e20
Show file tree
Hide file tree
Showing 112 changed files with 610 additions and 574 deletions.
12 changes: 8 additions & 4 deletions Mathbin/Algebra/Algebra/Basic.lean
View file
Expand Up @@ -722,7 +722,12 @@ end id

section PUnit

#print PUnit.algebra /-
/- warning: punit.algebra -> PUnit.algebra is a dubious translation:
lean 3 declaration is
forall {R : Type.{u}} [_inst_1 : CommSemiring.{u} R], Algebra.{u, u_1} R PUnit.{succ u_1} _inst_1 (Ring.toSemiring.{u_1} PUnit.{succ u_1} (CommRing.toRing.{u_1} PUnit.{succ u_1} PUnit.commRing.{u_1}))
but is expected to have type
forall {R : Type.{u}} [_inst_1 : CommSemiring.{u} R], Algebra.{u, 0} R PUnit.{1} _inst_1 (CommSemiring.toSemiring.{0} PUnit.{1} (CommRing.toCommSemiring.{0} PUnit.{1} PUnit.commRing.{0}))
Case conversion may be inaccurate. Consider using '#align punit.algebra PUnit.algebraₓ'. -/
instance PUnit.algebra : Algebra R PUnit
where
toFun x := PUnit.unit
Expand All @@ -733,13 +738,12 @@ instance PUnit.algebra : Algebra R PUnit
commutes' _ _ := rfl
smul_def' _ _ := rfl
#align punit.algebra PUnit.algebra
-/

/- warning: algebra.algebra_map_punit -> Algebra.algebraMap_pUnit is a dubious translation:
lean 3 declaration is
forall {R : Type.{u1}} [_inst_1 : CommSemiring.{u1} R] (r : R), Eq.{succ u2} PUnit.{succ u2} (coeFn.{max (succ u1) (succ u2), max (succ u1) (succ u2)} (RingHom.{u1, u2} R PUnit.{succ u2} (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u2} PUnit.{succ u2} (Ring.toSemiring.{u2} PUnit.{succ u2} (CommRing.toRing.{u2} PUnit.{succ u2} PUnit.commRing.{u2})))) (fun (_x : RingHom.{u1, u2} R PUnit.{succ u2} (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u2} PUnit.{succ u2} (Ring.toSemiring.{u2} PUnit.{succ u2} (CommRing.toRing.{u2} PUnit.{succ u2} PUnit.commRing.{u2})))) => R -> PUnit.{succ u2}) (RingHom.hasCoeToFun.{u1, u2} R PUnit.{succ u2} (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u2} PUnit.{succ u2} (Ring.toSemiring.{u2} PUnit.{succ u2} (CommRing.toRing.{u2} PUnit.{succ u2} PUnit.commRing.{u2})))) (algebraMap.{u1, u2} R PUnit.{succ u2} _inst_1 (Ring.toSemiring.{u2} PUnit.{succ u2} (CommRing.toRing.{u2} PUnit.{succ u2} PUnit.commRing.{u2})) (PUnit.algebra.{u1, u2} R _inst_1)) r) PUnit.unit.{succ u2}
forall {R : Type.{u}} [_inst_1 : CommSemiring.{u} R] (r : R), Eq.{succ u_1} PUnit.{succ u_1} (coeFn.{max (succ u) (succ u_1), max (succ u) (succ u_1)} (RingHom.{u, u_1} R PUnit.{succ u_1} (Semiring.toNonAssocSemiring.{u} R (CommSemiring.toSemiring.{u} R _inst_1)) (Semiring.toNonAssocSemiring.{u_1} PUnit.{succ u_1} (Ring.toSemiring.{u_1} PUnit.{succ u_1} (CommRing.toRing.{u_1} PUnit.{succ u_1} PUnit.commRing.{u_1})))) (fun (_x : RingHom.{u, u_1} R PUnit.{succ u_1} (Semiring.toNonAssocSemiring.{u} R (CommSemiring.toSemiring.{u} R _inst_1)) (Semiring.toNonAssocSemiring.{u_1} PUnit.{succ u_1} (Ring.toSemiring.{u_1} PUnit.{succ u_1} (CommRing.toRing.{u_1} PUnit.{succ u_1} PUnit.commRing.{u_1})))) => R -> PUnit.{succ u_1}) (RingHom.hasCoeToFun.{u, u_1} R PUnit.{succ u_1} (Semiring.toNonAssocSemiring.{u} R (CommSemiring.toSemiring.{u} R _inst_1)) (Semiring.toNonAssocSemiring.{u_1} PUnit.{succ u_1} (Ring.toSemiring.{u_1} PUnit.{succ u_1} (CommRing.toRing.{u_1} PUnit.{succ u_1} PUnit.commRing.{u_1})))) (algebraMap.{u, u_1} R PUnit.{succ u_1} _inst_1 (Ring.toSemiring.{u_1} PUnit.{succ u_1} (CommRing.toRing.{u_1} PUnit.{succ u_1} PUnit.commRing.{u_1})) (PUnit.algebra.{u, u_1} R _inst_1)) r) PUnit.unit.{succ u_1}
but is expected to have type
forall {R : Type.{u2}} [_inst_1 : CommSemiring.{u2} R] (r : R), Eq.{succ u1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => PUnit.{succ u1}) r) (FunLike.coe.{max (succ u2) (succ u1), succ u2, succ u1} (RingHom.{u2, u1} R PUnit.{succ u1} (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{u1} PUnit.{succ u1} (CommSemiring.toSemiring.{u1} PUnit.{succ u1} (CommRing.toCommSemiring.{u1} PUnit.{succ u1} PUnit.commRing.{u1})))) R (fun (_x : R) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => PUnit.{succ u1}) _x) (MulHomClass.toFunLike.{max u2 u1, u2, u1} (RingHom.{u2, u1} R PUnit.{succ u1} (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{u1} PUnit.{succ u1} (CommSemiring.toSemiring.{u1} PUnit.{succ u1} (CommRing.toCommSemiring.{u1} PUnit.{succ u1} PUnit.commRing.{u1})))) R PUnit.{succ u1} (NonUnitalNonAssocSemiring.toMul.{u2} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} R (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)))) (NonUnitalNonAssocSemiring.toMul.{u1} PUnit.{succ u1} (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} PUnit.{succ u1} (Semiring.toNonAssocSemiring.{u1} PUnit.{succ u1} (CommSemiring.toSemiring.{u1} PUnit.{succ u1} (CommRing.toCommSemiring.{u1} PUnit.{succ u1} PUnit.commRing.{u1}))))) (NonUnitalRingHomClass.toMulHomClass.{max u2 u1, u2, u1} (RingHom.{u2, u1} R PUnit.{succ u1} (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{u1} PUnit.{succ u1} (CommSemiring.toSemiring.{u1} PUnit.{succ u1} (CommRing.toCommSemiring.{u1} PUnit.{succ u1} PUnit.commRing.{u1})))) R PUnit.{succ u1} (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} R (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} PUnit.{succ u1} (Semiring.toNonAssocSemiring.{u1} PUnit.{succ u1} (CommSemiring.toSemiring.{u1} PUnit.{succ u1} (CommRing.toCommSemiring.{u1} PUnit.{succ u1} PUnit.commRing.{u1})))) (RingHomClass.toNonUnitalRingHomClass.{max u2 u1, u2, u1} (RingHom.{u2, u1} R PUnit.{succ u1} (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{u1} PUnit.{succ u1} (CommSemiring.toSemiring.{u1} PUnit.{succ u1} (CommRing.toCommSemiring.{u1} PUnit.{succ u1} PUnit.commRing.{u1})))) R PUnit.{succ u1} (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{u1} PUnit.{succ u1} (CommSemiring.toSemiring.{u1} PUnit.{succ u1} (CommRing.toCommSemiring.{u1} PUnit.{succ u1} PUnit.commRing.{u1}))) (RingHom.instRingHomClassRingHom.{u2, u1} R PUnit.{succ u1} (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{u1} PUnit.{succ u1} (CommSemiring.toSemiring.{u1} PUnit.{succ u1} (CommRing.toCommSemiring.{u1} PUnit.{succ u1} PUnit.commRing.{u1}))))))) (algebraMap.{u2, u1} R PUnit.{succ u1} _inst_1 (CommSemiring.toSemiring.{u1} PUnit.{succ u1} (CommRing.toCommSemiring.{u1} PUnit.{succ u1} PUnit.commRing.{u1})) (PUnit.algebra.{u2, u1} R _inst_1)) r) PUnit.unit.{succ u1}
forall {R : Type.{u}} [_inst_1 : CommSemiring.{u} R] (r : R), Eq.{1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => PUnit.{1}) r) (FunLike.coe.{succ u, succ u, 1} (RingHom.{u, 0} R PUnit.{1} (Semiring.toNonAssocSemiring.{u} R (CommSemiring.toSemiring.{u} R _inst_1)) (Semiring.toNonAssocSemiring.{0} PUnit.{1} (CommSemiring.toSemiring.{0} PUnit.{1} (CommRing.toCommSemiring.{0} PUnit.{1} PUnit.commRing.{0})))) R (fun (_x : R) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => PUnit.{1}) _x) (MulHomClass.toFunLike.{u, u, 0} (RingHom.{u, 0} R PUnit.{1} (Semiring.toNonAssocSemiring.{u} R (CommSemiring.toSemiring.{u} R _inst_1)) (Semiring.toNonAssocSemiring.{0} PUnit.{1} (CommSemiring.toSemiring.{0} PUnit.{1} (CommRing.toCommSemiring.{0} PUnit.{1} PUnit.commRing.{0})))) R PUnit.{1} (NonUnitalNonAssocSemiring.toMul.{u} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u} R (Semiring.toNonAssocSemiring.{u} R (CommSemiring.toSemiring.{u} R _inst_1)))) (NonUnitalNonAssocSemiring.toMul.{0} PUnit.{1} (NonAssocSemiring.toNonUnitalNonAssocSemiring.{0} PUnit.{1} (Semiring.toNonAssocSemiring.{0} PUnit.{1} (CommSemiring.toSemiring.{0} PUnit.{1} (CommRing.toCommSemiring.{0} PUnit.{1} PUnit.commRing.{0}))))) (NonUnitalRingHomClass.toMulHomClass.{u, u, 0} (RingHom.{u, 0} R PUnit.{1} (Semiring.toNonAssocSemiring.{u} R (CommSemiring.toSemiring.{u} R _inst_1)) (Semiring.toNonAssocSemiring.{0} PUnit.{1} (CommSemiring.toSemiring.{0} PUnit.{1} (CommRing.toCommSemiring.{0} PUnit.{1} PUnit.commRing.{0})))) R PUnit.{1} (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u} R (Semiring.toNonAssocSemiring.{u} R (CommSemiring.toSemiring.{u} R _inst_1))) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{0} PUnit.{1} (Semiring.toNonAssocSemiring.{0} PUnit.{1} (CommSemiring.toSemiring.{0} PUnit.{1} (CommRing.toCommSemiring.{0} PUnit.{1} PUnit.commRing.{0})))) (RingHomClass.toNonUnitalRingHomClass.{u, u, 0} (RingHom.{u, 0} R PUnit.{1} (Semiring.toNonAssocSemiring.{u} R (CommSemiring.toSemiring.{u} R _inst_1)) (Semiring.toNonAssocSemiring.{0} PUnit.{1} (CommSemiring.toSemiring.{0} PUnit.{1} (CommRing.toCommSemiring.{0} PUnit.{1} PUnit.commRing.{0})))) R PUnit.{1} (Semiring.toNonAssocSemiring.{u} R (CommSemiring.toSemiring.{u} R _inst_1)) (Semiring.toNonAssocSemiring.{0} PUnit.{1} (CommSemiring.toSemiring.{0} PUnit.{1} (CommRing.toCommSemiring.{0} PUnit.{1} PUnit.commRing.{0}))) (RingHom.instRingHomClassRingHom.{u, 0} R PUnit.{1} (Semiring.toNonAssocSemiring.{u} R (CommSemiring.toSemiring.{u} R _inst_1)) (Semiring.toNonAssocSemiring.{0} PUnit.{1} (CommSemiring.toSemiring.{0} PUnit.{1} (CommRing.toCommSemiring.{0} PUnit.{1} PUnit.commRing.{0}))))))) (algebraMap.{u, 0} R PUnit.{1} _inst_1 (CommSemiring.toSemiring.{0} PUnit.{1} (CommRing.toCommSemiring.{0} PUnit.{1} PUnit.commRing.{0})) (PUnit.algebra.{u} R _inst_1)) r) PUnit.unit.{1}
Case conversion may be inaccurate. Consider using '#align algebra.algebra_map_punit Algebra.algebraMap_pUnitₓ'. -/
@[simp]
theorem algebraMap_pUnit (r : R) : algebraMap R PUnit r = PUnit.unit :=
Expand Down
14 changes: 7 additions & 7 deletions Mathbin/Algebra/Algebra/Subalgebra/Basic.lean
View file

Large diffs are not rendered by default.

0 comments on commit b356e20

Please sign in to comment.