Commit 2024-08-08 06:02 15720c78

View on Github →

chore: backports for leanprover/lean4#4814 (part 20) (#15440) see https://github.com/leanprover-community/mathlib4/pull/15245

Estimated changes

modified theorem CocompactMapClass.norm_le
modified theorem Submodule.finrank_map_le
modified theorem natCast_le_rank_iff
modified theorem natCast_le_rank_iff_finset
modified theorem IsIntegral.of_pow
modified theorem isIntegral_algHom_iff
modified theorem isIntegral_one
modified theorem isIntegral_zero
modified theorem ValuationRing.of_integers
modified theorem subset_mul_closure_one
modified theorem TopCat.Sheaf.extend_hom_app
modified theorem TopCat.Sheaf.hom_ext