group_with_zero): mark `has_continuous_inv₀` as a `Prop` (#12770)

Commit

3 years ago

chore(topology/algebra/group_with_zero): mark `has_continuous_inv₀` as a `Prop` (#12770) Since the type was not explicitly given, Lean marked this as a `Type`.

Author

j-loreaux

Parents

3e6e34e4

mathlib3 2cb5edb5 - chore(topology/algebra/group_with_zero): mark `has_continuous_inv₀` as a `Prop` (#12770)

mathlib3
2cb5edb5 - chore(topology/algebra/group_with_zero): mark `has_continuous_inv₀` as a `Prop` (#12770)