feat(RepresentationTheory): add Ado theorem problems

[kim-em]

Summary

• add Ado theorem in characteristic zero as a faithful finite-dimensional Lie representation problem
• add the Ado–Iwasawa theorem over an arbitrary field as a separate problem
• include source notes and proof sketches following the Tau Ceti Ado–Iwasawa roadmap
• provide the commutator Lie-ring instance needed by standalone generated workspaces

Roadmap context: TauCetiProject/TauCetiRoadmap#102

Validation

• lake exe lean-eval validate-manifest
• lake exe lean-eval check-problem-build
• generated and built adoCharZero workspace
• generated and built adoIwasawa workspace
• git diff --check