Theorem FaithfulSMul.of_injective

Modification history

2025-02-07 20:57
Mathlib/GroupTheory/GroupAction/Hom.lean
feat(Mathlib/Algebra/Azumaya/Basic): More on azumaya (#21446) …
Added FaithfulSMul.of_injectiveView on Github →