mathlib

853192ce - feat(topology/algebra): Inf and inducing preserve compatibility with algebraic structure (#11720)

feat(topology/algebra): Inf and inducing preserve compatibility with algebraic structure (#11720) This partly duplicates @mariainesdff 's work on group topologies, but I'm using an unbundled approach which avoids defining a new `X_topology` structure for each interesting X.