Commit 2024-02-25 13:35 a3692d91

View on Github →

fix(Algebra/DirectSum/Ring): correct mis-ported lemma names (#10953)

Estimated changes

deleted theorem DirectSum.ofIntCast
deleted theorem DirectSum.ofNatCast
added theorem DirectSum.of_intCast
added theorem DirectSum.of_natCast