Commit 2025-01-10 18:19 acc35eb4

View on Github →

chore: make FooHom.coe_id a norm_cast lemma (#20576) From GrowthInGroups (LeanCamCombi)

Estimated changes

Modified Mathlib/Algebra/Algebra/Hom.lean

Modified Mathlib/Algebra/Algebra/NonUnitalHom.lean

Modified Mathlib/Algebra/Lie/Basic.lean

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

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

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

Modified Mathlib/Algebra/Star/StarAlgHom.lean

Modified Mathlib/Algebra/Star/StarRingHom.lean

Modified Mathlib/Analysis/Normed/Affine/Isometry.lean

Modified Mathlib/Analysis/Normed/Operator/LinearIsometry.lean

Modified Mathlib/Data/PFun.lean

Modified Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean

Modified Mathlib/Order/Heyting/Hom.lean

Modified Mathlib/Order/Hom/Bounded.lean

Modified Mathlib/Order/Hom/CompleteLattice.lean

Modified Mathlib/Order/Hom/Lattice.lean

Modified Mathlib/RingTheory/Bialgebra/Hom.lean

Modified Mathlib/RingTheory/Coalgebra/Hom.lean

Modified Mathlib/Topology/Bornology/Hom.lean

Modified Mathlib/Topology/ContinuousMap/Basic.lean

Modified Mathlib/Topology/ContinuousMap/CocompactMap.lean

Modified Mathlib/Topology/Hom/Open.lean

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

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

Modified Mathlib/Topology/Spectral/Hom.lean