Commit 2021-09-06 12:25 893c4746

View on Github →

feat(group_theory/submonoid/membership): add log, exp lemmas (#8870) Breaking up a previous PR (#7843) into smaller ones. This PR adds lemmas about injectivity of pow and log functions under appropriate conditions. Zulip

Estimated changes

Modified src/group_theory/submonoid/membership.lean

added def submonoid.log

added theorem submonoid.log_pow_eq_self

added theorem submonoid.log_pow_int_eq_self

added def submonoid.pow

added theorem submonoid.pow_log_eq_self

added theorem submonoid.pow_right_injective_iff_pow_injective