Commit 2025-02-10 08:08 5499530e

View on Github →

chore: normalize comments for issue #10675 (#21628)

Estimated changes

Modified Mathlib/Algebra/Category/Ring/Adjunctions.lean

Modified Mathlib/Algebra/Lie/Submodule.lean

modified theorem LieModuleEquiv.ofTop_apply

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

Modified Mathlib/Data/Fin/Basic.lean

Modified Mathlib/Topology/Specialization.lean

modified theorem Specialization.ofEquiv_inj

modified theorem Specialization.toEquiv_inj