Commit 2023-04-13 20:39 1cd8b316

View on Github →

chore: bump to nightly-2023-04-11 (#3139)

Estimated changes

Modified Mathlib/Algebra/AddTorsor.lean

Modified Mathlib/Algebra/Algebra/Equiv.lean

Modified Mathlib/Algebra/Algebra/Hom.lean

Modified Mathlib/Algebra/Category/ModuleCat/Basic.lean

Modified Mathlib/Algebra/EuclideanDomain/Basic.lean

Modified Mathlib/Algebra/Hom/Equiv/Basic.lean

Modified Mathlib/Algebra/Hom/Group.lean

modified theorem MonoidHom.comp_inv

modified theorem MonoidHom.div_apply

modified theorem MonoidHom.inv_apply

modified theorem MonoidHom.inv_comp

modified theorem MonoidHom.mul_apply

modified theorem MulHom.mul_apply

Modified Mathlib/Algebra/Hom/NonUnitalAlg.lean

Modified Mathlib/Algebra/Hom/Ring.lean

Modified Mathlib/Algebra/Module/Equiv.lean

Modified Mathlib/Algebra/Module/LinearMap.lean

Modified Mathlib/Algebra/Module/Pi.lean

Modified Mathlib/Algebra/Module/Prod.lean

Modified Mathlib/Algebra/Order/Hom/Basic.lean

Modified Mathlib/Algebra/Order/Hom/Ring.lean

Modified Mathlib/Algebra/Ring/Equiv.lean

Modified Mathlib/Algebra/Star/StarAlgHom.lean

Modified Mathlib/Analysis/Normed/Field/Basic.lean

Modified Mathlib/Analysis/Normed/Group/Basic.lean

modified theorem Submodule.coe_norm

modified theorem Submodule.norm_coe

Modified Mathlib/Analysis/Normed/Group/Seminorm.lean

Modified Mathlib/CategoryTheory/ConcreteCategory/BundledHom.lean

Modified Mathlib/CategoryTheory/Over.lean

modified def CategoryTheory.Over.coeFromHom

Modified Mathlib/Combinatorics/Catalan.lean

Modified Mathlib/Data/Analysis/Topology.lean

Modified Mathlib/Data/MvPolynomial/Equiv.lean

Modified Mathlib/Data/Nat/Fib.lean

Modified Mathlib/Data/PNat/Xgcd.lean

Modified Mathlib/GroupTheory/GroupAction/Basic.lean

Modified Mathlib/GroupTheory/GroupAction/Prod.lean

Modified Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean

Modified Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean

Modified Mathlib/LinearAlgebra/Basis.lean

Modified Mathlib/LinearAlgebra/FinsuppVectorSpace.lean

Modified Mathlib/LinearAlgebra/Ray.lean

Modified Mathlib/LinearAlgebra/SesquilinearForm.lean

Modified Mathlib/ModelTheory/Basic.lean

Modified Mathlib/Order/Heyting/Hom.lean

Modified Mathlib/Order/Hom/Basic.lean

modified def OrderIsoClass.toOrderIso

Modified Mathlib/Order/Hom/Bounded.lean

Modified Mathlib/Order/Hom/CompleteLattice.lean

Modified Mathlib/Order/Hom/Lattice.lean

Modified Mathlib/Order/RelClasses.lean

Modified Mathlib/RingTheory/SimpleModule.lean

Modified Mathlib/Topology/Algebra/ConstMulAction.lean

Modified Mathlib/Topology/Algebra/Module/Basic.lean

Modified Mathlib/Topology/Order/Hom/Basic.lean

Modified Mathlib/Topology/Spectral/Hom.lean

Modified lake-manifest.json

Modified lean-toolchain