Skip to content

Commit

Permalink
bump to nightly-2023-03-24-16
Browse files Browse the repository at this point in the history 
mathlib commit leanprover-community/mathlib@b19481d
  • Loading branch information
@leanprover-community-bot
leanprover-community-bot committed Mar 24, 2023
1 parent 4fed16d commit 5b87f9b
Show file tree
Hide file tree
Showing 48 changed files with 1,942 additions and 461 deletions.
2 changes: 1 addition & 1 deletion Mathbin/Algebra/Algebra/Basic.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -964,7 +964,7 @@ instance : Algebra R Aᵐᵒᵖ :=
lean 3 declaration is
forall {R : Type.{u1}} {A : Type.{u2}} [_inst_1 : CommSemiring.{u1} R] [_inst_2 : Semiring.{u2} A] [_inst_3 : Algebra.{u1, u2} R A _inst_1 _inst_2] (c : R), Eq.{succ u2} (MulOpposite.{u2} A) (coeFn.{max (succ u1) (succ u2), max (succ u1) (succ u2)} (RingHom.{u1, u2} R (MulOpposite.{u2} A) (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u2} (MulOpposite.{u2} A) (MulOpposite.semiring.{u2} A _inst_2))) (fun (_x : RingHom.{u1, u2} R (MulOpposite.{u2} A) (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u2} (MulOpposite.{u2} A) (MulOpposite.semiring.{u2} A _inst_2))) => R -> (MulOpposite.{u2} A)) (RingHom.hasCoeToFun.{u1, u2} R (MulOpposite.{u2} A) (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u2} (MulOpposite.{u2} A) (MulOpposite.semiring.{u2} A _inst_2))) (algebraMap.{u1, u2} R (MulOpposite.{u2} A) _inst_1 (MulOpposite.semiring.{u2} A _inst_2) (MulOpposite.algebra.{u1, u2} R A _inst_1 _inst_2 _inst_3)) c) (MulOpposite.op.{u2} A (coeFn.{max (succ u1) (succ u2), max (succ u1) (succ u2)} (RingHom.{u1, u2} R A (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u2} A _inst_2)) (fun (_x : RingHom.{u1, u2} R A (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u2} A _inst_2)) => R -> A) (RingHom.hasCoeToFun.{u1, u2} R A (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u2} A _inst_2)) (algebraMap.{u1, u2} R A _inst_1 _inst_2 _inst_3) c))
but is expected to have type
forall {R : Type.{u1}} {A : Type.{u2}} [_inst_1 : CommSemiring.{u1} R] [_inst_2 : Semiring.{u2} A] [_inst_3 : Algebra.{u1, u2} R A _inst_1 _inst_2] (c : R), Eq.{succ u2} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => MulOpposite.{u2} A) c) (FunLike.coe.{max (succ u1) (succ u2), succ u1, succ u2} (RingHom.{u1, u2} R (MulOpposite.{u2} A) (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u2} (MulOpposite.{u2} A) (MulOpposite.instSemiringMulOpposite.{u2} A _inst_2))) R (fun (_x : R) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => MulOpposite.{u2} A) _x) (MulHomClass.toFunLike.{max u1 u2, u1, u2} (RingHom.{u1, u2} R (MulOpposite.{u2} A) (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u2} (MulOpposite.{u2} A) (MulOpposite.instSemiringMulOpposite.{u2} A _inst_2))) R (MulOpposite.{u2} A) (NonUnitalNonAssocSemiring.toMul.{u1} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)))) (NonUnitalNonAssocSemiring.toMul.{u2} (MulOpposite.{u2} A) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} (MulOpposite.{u2} A) (Semiring.toNonAssocSemiring.{u2} (MulOpposite.{u2} A) (MulOpposite.instSemiringMulOpposite.{u2} A _inst_2)))) (NonUnitalRingHomClass.toMulHomClass.{max u1 u2, u1, u2} (RingHom.{u1, u2} R (MulOpposite.{u2} A) (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u2} (MulOpposite.{u2} A) (MulOpposite.instSemiringMulOpposite.{u2} A _inst_2))) R (MulOpposite.{u2} A) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1))) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} (MulOpposite.{u2} A) (Semiring.toNonAssocSemiring.{u2} (MulOpposite.{u2} A) (MulOpposite.instSemiringMulOpposite.{u2} A _inst_2))) (RingHomClass.toNonUnitalRingHomClass.{max u1 u2, u1, u2} (RingHom.{u1, u2} R (MulOpposite.{u2} A) (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u2} (MulOpposite.{u2} A) (MulOpposite.instSemiringMulOpposite.{u2} A _inst_2))) R (MulOpposite.{u2} A) (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u2} (MulOpposite.{u2} A) (MulOpposite.instSemiringMulOpposite.{u2} A _inst_2)) (RingHom.instRingHomClassRingHom.{u1, u2} R (MulOpposite.{u2} A) (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u2} (MulOpposite.{u2} A) (MulOpposite.instSemiringMulOpposite.{u2} A _inst_2)))))) (algebraMap.{u1, u2} R (MulOpposite.{u2} A) _inst_1 (MulOpposite.instSemiringMulOpposite.{u2} A _inst_2) (MulOpposite.instAlgebraMulOppositeInstSemiringMulOpposite.{u1, u2} R A _inst_1 _inst_2 _inst_3)) c) (MulOpposite.op.{u2} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => A) c) (FunLike.coe.{max (succ u1) (succ u2), succ u1, succ u2} (RingHom.{u1, u2} R A (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u2} A _inst_2)) R (fun (_x : R) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => A) _x) (MulHomClass.toFunLike.{max u1 u2, u1, u2} (RingHom.{u1, u2} R A (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u2} A _inst_2)) R A (NonUnitalNonAssocSemiring.toMul.{u1} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)))) (NonUnitalNonAssocSemiring.toMul.{u2} A (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} A (Semiring.toNonAssocSemiring.{u2} A _inst_2))) (NonUnitalRingHomClass.toMulHomClass.{max u1 u2, u1, u2} (RingHom.{u1, u2} R A (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u2} A _inst_2)) R A (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1))) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} A (Semiring.toNonAssocSemiring.{u2} A _inst_2)) (RingHomClass.toNonUnitalRingHomClass.{max u1 u2, u1, u2} (RingHom.{u1, u2} R A (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u2} A _inst_2)) R A (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u2} A _inst_2) (RingHom.instRingHomClassRingHom.{u1, u2} R A (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u2} A _inst_2))))) (algebraMap.{u1, u2} R A _inst_1 _inst_2 _inst_3) c))
forall {R : Type.{u1}} {A : Type.{u2}} [_inst_1 : CommSemiring.{u1} R] [_inst_2 : Semiring.{u2} A] [_inst_3 : Algebra.{u1, u2} R A _inst_1 _inst_2] (c : R), Eq.{succ u2} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => MulOpposite.{u2} A) c) (FunLike.coe.{max (succ u1) (succ u2), succ u1, succ u2} (RingHom.{u1, u2} R (MulOpposite.{u2} A) (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u2} (MulOpposite.{u2} A) (MulOpposite.semiring.{u2} A _inst_2))) R (fun (_x : R) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => MulOpposite.{u2} A) _x) (MulHomClass.toFunLike.{max u1 u2, u1, u2} (RingHom.{u1, u2} R (MulOpposite.{u2} A) (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u2} (MulOpposite.{u2} A) (MulOpposite.semiring.{u2} A _inst_2))) R (MulOpposite.{u2} A) (NonUnitalNonAssocSemiring.toMul.{u1} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)))) (NonUnitalNonAssocSemiring.toMul.{u2} (MulOpposite.{u2} A) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} (MulOpposite.{u2} A) (Semiring.toNonAssocSemiring.{u2} (MulOpposite.{u2} A) (MulOpposite.semiring.{u2} A _inst_2)))) (NonUnitalRingHomClass.toMulHomClass.{max u1 u2, u1, u2} (RingHom.{u1, u2} R (MulOpposite.{u2} A) (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u2} (MulOpposite.{u2} A) (MulOpposite.semiring.{u2} A _inst_2))) R (MulOpposite.{u2} A) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1))) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} (MulOpposite.{u2} A) (Semiring.toNonAssocSemiring.{u2} (MulOpposite.{u2} A) (MulOpposite.semiring.{u2} A _inst_2))) (RingHomClass.toNonUnitalRingHomClass.{max u1 u2, u1, u2} (RingHom.{u1, u2} R (MulOpposite.{u2} A) (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u2} (MulOpposite.{u2} A) (MulOpposite.semiring.{u2} A _inst_2))) R (MulOpposite.{u2} A) (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u2} (MulOpposite.{u2} A) (MulOpposite.semiring.{u2} A _inst_2)) (RingHom.instRingHomClassRingHom.{u1, u2} R (MulOpposite.{u2} A) (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u2} (MulOpposite.{u2} A) (MulOpposite.semiring.{u2} A _inst_2)))))) (algebraMap.{u1, u2} R (MulOpposite.{u2} A) _inst_1 (MulOpposite.semiring.{u2} A _inst_2) (MulOpposite.instAlgebraMulOppositeSemiring.{u1, u2} R A _inst_1 _inst_2 _inst_3)) c) (MulOpposite.op.{u2} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => A) c) (FunLike.coe.{max (succ u1) (succ u2), succ u1, succ u2} (RingHom.{u1, u2} R A (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u2} A _inst_2)) R (fun (_x : R) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => A) _x) (MulHomClass.toFunLike.{max u1 u2, u1, u2} (RingHom.{u1, u2} R A (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u2} A _inst_2)) R A (NonUnitalNonAssocSemiring.toMul.{u1} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)))) (NonUnitalNonAssocSemiring.toMul.{u2} A (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} A (Semiring.toNonAssocSemiring.{u2} A _inst_2))) (NonUnitalRingHomClass.toMulHomClass.{max u1 u2, u1, u2} (RingHom.{u1, u2} R A (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u2} A _inst_2)) R A (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1))) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} A (Semiring.toNonAssocSemiring.{u2} A _inst_2)) (RingHomClass.toNonUnitalRingHomClass.{max u1 u2, u1, u2} (RingHom.{u1, u2} R A (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u2} A _inst_2)) R A (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u2} A _inst_2) (RingHom.instRingHomClassRingHom.{u1, u2} R A (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u2} A _inst_2))))) (algebraMap.{u1, u2} R A _inst_1 _inst_2 _inst_3) c))
Case conversion may be inaccurate. Consider using '#align mul_opposite.algebra_map_apply MulOpposite.algebraMap_applyₓ'. -/
@[simp]
theorem algebraMap_apply (c : R) : algebraMap R Aᵐᵒᵖ c = op (algebraMap R A c) :=
Expand Down
26 changes: 13 additions & 13 deletions Mathbin/Algebra/Algebra/Operations.lean
View file

Large diffs are not rendered by default.

Loading

0 comments on commit 5b87f9b

Please sign in to comment.