# Dot notation

Say you have a type, like `subgroup G`

, and a term of that type, like `H : subgroup G`

. Say you have a function in the `subgroup`

namespace which takes as input a term of type `subgroup G`

, for example `subgroup.inv_mem`

, which has as an explicit input a term `H : subgroup G`

and spits out a proof that `x ∈ H → x⁻¹ ∈ H`

. Then instead of writing `subgroup.inv_mem H : x ∈ H → x⁻¹ ∈ H`

you can just write `H.inv_mem : x ∈ H → x⁻¹ ∈ H`

.

In general the rule is that if you have a term `H : foo ...`

of type `foo`

or `foo A B`

or whatever, and then you have a function called `foo.bar`

which has an explicit (i.e., round brackets) input of type `foo ...`

, then instead of `foo.bar H`

you can just write `H.bar`

. This is why it’s a good idea to define theorems about `foo``s in the ``foo`

namespace.

This sort of trick can be used all over the place; it’s surprisingly powerful. For example Lean has a proof `eq.symm : x = y → y = x`

. If you have a term `h : a = b`

then, remembering that `=`

is just notation for `eq`

so that `h`

really has type `eq a b`

, you can write `h.symm : b = a`

as shorthand for `eq.symm h`

.