Skip to content

Commit

Permalink
chore(Topology/Algebra): add missing #aligns (#10307)
Browse files Browse the repository at this point in the history
  • Loading branch information
urkud committed Feb 7, 2024
1 parent 92e0962 commit b4f55ab
Showing 1 changed file with 4 additions and 0 deletions.
4 changes: 4 additions & 0 deletions Mathlib/Topology/Algebra/Constructions.lean
Expand Up @@ -53,7 +53,11 @@ def opHomeomorph : M ≃ₜ Mᵐᵒᵖ where
continuous_toFun := continuous_op
continuous_invFun := continuous_unop
#align mul_opposite.op_homeomorph MulOpposite.opHomeomorph
#align mul_opposite.op_homeomorph_apply MulOpposite.opHomeomorph_apply
#align mul_opposite.op_homeomorph_symm_apply MulOpposite.opHomeomorph_symm_apply
#align add_opposite.op_homeomorph AddOpposite.opHomeomorph
#align add_opposite.op_homeomorph_apply AddOpposite.opHomeomorph_apply
#align add_opposite.op_homeomorph_symm_apply AddOpposite.opHomeomorph_symm_apply

@[to_additive]
instance instT2Space [T2Space M] : T2Space Mᵐᵒᵖ :=
Expand Down

0 comments on commit b4f55ab

Please sign in to comment.