Commit 2022-08-29 13:10 daec7d61

View on Github →

chore(order/bounded_order): Rename is_complemented to complemented_lattice (#16263) This is to make space for the predicate is_complemented : α → Prop := ∃ b, is_compl a b.

Estimated changes

Modified src/linear_algebra/basis.lean

Modified src/order/atoms.lean

added theorem is_atomic_of_is_coatomic_of_complemented_lattice_of_is_modular

deleted theorem is_atomic_of_is_coatomic_of_is_complemented_of_is_modular

added theorem is_coatomic_of_is_atomic_of_complemented_lattice_of_is_modular

deleted theorem is_coatomic_of_is_atomic_of_is_complemented_of_is_modular

Modified src/order/boolean_algebra.lean

Modified src/order/bounded_order.lean

Modified src/order/compactly_generated.lean

added theorem complemented_lattice_iff_is_atomistic

added theorem complemented_lattice_of_Sup_atoms_eq_top

added theorem complemented_lattice_of_is_atomistic

deleted theorem is_complemented_iff_is_atomistic

deleted theorem is_complemented_of_Sup_atoms_eq_top

deleted theorem is_complemented_of_is_atomistic

Modified src/order/hom/basic.lean

added theorem order_iso.complemented_lattice

added theorem order_iso.complemented_lattice_iff

deleted theorem order_iso.is_complemented

deleted theorem order_iso.is_complemented_iff

Modified src/order/modular_lattice.lean

Modified src/representation_theory/maschke.lean

Modified src/ring_theory/simple_module.lean

modified def is_semisimple_module