Theorem Function.Bijective.of_comp_left

Modification history

2026-06-20 15:40
Mathlib/Logic/Function/Basic.lean
refactor(FieldTheory/Galois/IsGaloisGroup): generalize `mulEquivAlgEquiv` to domains (#40822) …
Added Function.Bijective.of_comp_leftView on Github →