Merge branch 'fix/missing-include-amg' into 'master'

[fix][amg] Add missing include

See merge request !2738

(cherry picked from commit 0c8d203e)

707dc14b [fix][amg] Add missing include
5 jobs for !2742 with cherry-pick-0c8d203e
latest detached
Status Name Job ID Coverage
  Trigger
manual full-dune-2.7-clang
manual full-dune-2.7-gcc
manual full-dune-master-gcc
manual minimal-dune-2.7-gcc
 
  Downstream Modules
created trigger lecture