Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-03-25 19:21 291a4f35

View on Github →

refactor(algebra/group_action): use notation for monoid/group actions (#846)

refactor(module_action): bundle and introduce notation
fix(linear_algebra/determinant): fix the coercion issue using a local notation
fix(linear_algebra/dimension): fix build

Estimated changes

Modified src/algebra/module.lean

Modified src/group_theory/group_action.lean

added theorem group_action.bijective

added def group_action.comp_hom

added def group_action.mul_left_cosets

added theorem group_action.orbit_eq_iff

added def group_action.orbit_rel

added def group_action.to_perm

deleted theorem is_group_action.bijective

deleted theorem is_group_action.comp_hom

deleted def is_group_action.mul_left_cosets

deleted theorem is_group_action.orbit_eq_iff

deleted def is_group_action.orbit_rel

deleted def is_group_action.to_perm

deleted theorem is_monoid_action.comp_hom

deleted def is_monoid_action.fixed_points

deleted theorem is_monoid_action.mem_fixed_points'

deleted theorem is_monoid_action.mem_fixed_points

deleted theorem is_monoid_action.mem_orbit

deleted theorem is_monoid_action.mem_orbit_iff

deleted theorem is_monoid_action.mem_orbit_self

deleted theorem is_monoid_action.mem_stabilizer_iff

deleted def is_monoid_action.orbit

deleted def is_monoid_action.stabilizer

added def monoid_action.comp_hom

added def monoid_action.fixed_points

added theorem monoid_action.mem_fixed_points'

added theorem monoid_action.mem_fixed_points

added theorem monoid_action.mem_orbit

added theorem monoid_action.mem_orbit_iff

added theorem monoid_action.mem_orbit_self

added theorem monoid_action.mem_stabilizer_iff

added def monoid_action.orbit

added def monoid_action.stabilizer

Modified src/group_theory/sylow.lean

added theorem group_action.card_modeq_card_fixed_points

added theorem group_action.mem_fixed_points_iff_card_orbit_eq_one

deleted theorem is_group_action.card_modeq_card_fixed_points

deleted theorem is_group_action.mem_fixed_points_iff_card_orbit_eq_one

Modified src/linear_algebra/determinant.lean

Modified src/linear_algebra/dimension.lean