where is the code for group.to_monoid

Stream: Is there code for X?

[Lars Ericson]

If I go to group.to_monoid, the doc exists. When I press on source, the string to_monoid occurs 0 times in the source code. Yet if I do

import algebra.group.defs
#check group.to_monoid -- group.to_monoid : Π (α : Type u_1) [s : group α], monoid α

it is there. How does it get implemented? If a class B extends a class A, does A.to_B automatically get defined?

[Alex J. Best]

That's right, its automatically generated, when you extend structures the extending structure has all the fields of the structure being extended so to_blah can be done by just restricting to those fields.
In this case even though its not written anywhere we can still #print it to see what it is

set_option pp.proofs true
#print group.to_monoid

gives

@[instance, priority 100, to_additive_aux id.{1} name add_group.to_add_monoid]
def group.to_monoid : Π (α : Type u) [s : group α], monoid α :=
λ (α : Type u) [s : group α],
  {mul := group.mul s,
   mul_assoc := group.mul_assoc s,
   one := group.one s,
   one_mul := group.one_mul s,
   mul_one := group.mul_one s}