[Merged by Bors] - feat(RingTheory/LocalRing/ResidueField/Basic): add algebra homs between residue fields#39716

tb65536 wants to merge 3 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

tb65536:tb_locrngmap943tb65536/mathlib4:tb_locrngmap943Copy head branch name to clipboard