Documentation

RenamingSets.RenameAction.Basic

source
@[simp]
theorem RenamingSets.rename_one' {𝔸 : Type u_1} {X : Type u_2} [RenameAction 𝔸 X] :
rename 1 = id
source
@[simp]
theorem RenamingSets.rename_discrete' {𝔸 : Type u_1} {X : Type u_2} [RenameAction 𝔸 X] [DiscreteRenameAction 𝔸 X] (σ : Ren 𝔸) :
rename σ = id
source
instance RenamingSets.instDiscreteRenameAction {𝔸 : Type u_1} {X : Type u_2} :
DiscreteRenameAction 𝔸 X