Commit 2022-08-31 20:06 9b68ed5e

View on Github →

refactor(topology/algebra/continuous_monoid_hom): Make variables consistent (#16304) This PR cleans up some redundant variables in continuous_monoid_hom.

Estimated changes

Modified src/topology/algebra/continuous_monoid_hom.lean

modified def continuous_monoid_hom.to_continuous_map

modified theorem continuous_monoid_hom.to_continuous_map_injective

modified def pontryagin_dual